[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
letI := NormedAddCommGroup.ofMatrix hS.transpose
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
letI := InnerProductSpace.ofMatrix hS.transpose
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix (_ : PosDef Sᵀ)
⊢ lowerInv hS = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix (_ : PosDef Sᵀ)
i j : n
⊢ lowerInv hS i j = (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ i j
[PROOFSTEP]
rw [LDL.lowerInv, Basis.coePiBasisFun.toMatrix_eq_transpose, coe_gramSchmidtBasis]
[GOAL]
case a.h
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this✝ : NormedAddCommGroup (n → 𝕜) := NormedAddCommGroup.ofMatrix (_ : PosDef Sᵀ)
this : InnerProductSpace 𝕜 (n → 𝕜) := InnerProductSpace.ofMatrix (_ : PosDef Sᵀ)
i j : n
⊢ gramSchmidt 𝕜 (↑(Pi.basisFun 𝕜 n)) i j = (gramSchmidt 𝕜 ↑(Pi.basisFun 𝕜 n))ᵀᵀ i j
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ Invertible (lowerInv hS)
[PROOFSTEP]
rw [LDL.lowerInv_eq_gramSchmidtBasis]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ Invertible (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
haveI :=
  Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
    (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (_ : _) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _ (Pi.basisFun 𝕜 n))
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
this : Invertible (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))
⊢ Invertible (Basis.toMatrix (Pi.basisFun 𝕜 n) ↑(gramSchmidtBasis (Pi.basisFun 𝕜 n)))ᵀ
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : i < j
⊢ lowerInv hS i j = 0
[PROOFSTEP]
rw [←
  @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (_ : _) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _ i j hij
    (Pi.basisFun 𝕜 n),
  Pi.basisFun_repr, LDL.lowerInv]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
[PROOFSTEP]
simp only [diag, diagEntries, EuclideanSpace.inner_piLp_equiv_symm, star_star, hij, diagonal_apply_eq, Matrix.mul_assoc]
[GOAL]
case pos
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : i = j
⊢ lowerInv hS j ⬝ᵥ mulVec S (star (lowerInv hS j)) = (lowerInv hS * (S * (lowerInv hS)ᴴ)) j j
[PROOFSTEP]
rfl
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : ¬i = j
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j
[PROOFSTEP]
simp only [LDL.diag, hij, diagonal_apply_ne, Ne.def, not_false_iff, mul_mul_apply]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : ¬i = j
⊢ 0 = lowerInv hS i ⬝ᵥ mulVec S ((lowerInv hS)ᴴᵀ j)
[PROOFSTEP]
rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
  (LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm, mulVec_transpose,
  EuclideanSpace.inner_piLp_equiv_symm, ← IsROrC.star_def, ← star_dotProduct_star, dotProduct_comm, star_star]
[GOAL]
case neg
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
i j : n
hij : ¬i = j
⊢ vecMul (lowerInv hS i) S ⬝ᵥ star (lowerInv hS j) = vecMul (lowerInv hS i) S ⬝ᵥ map (lowerInv hS) star j
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ lower hS * diag hS * (lower hS)ᴴ = S
[PROOFSTEP]
rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
  Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS), Matrix.mul_inv_eq_iff_eq_mul_of_invertible]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : IsWellOrder n fun x x_1 => x < x_1
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : PosDef S
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
[PROOFSTEP]
exact LDL.diag_eq_lowerInv_conj hS


[GOAL]
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
⊢ ↑(toMatrix (Basis.dualBasis B₂) (Basis.dualBasis B₁)) (↑Module.Dual.transpose u) = (↑(toMatrix B₁ B₂) u)ᵀ
[PROOFSTEP]
ext i j
[GOAL]
case a.h
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
u : V₁ →ₗ[K] V₂
i : ι₁
j : ι₂
⊢ ↑(toMatrix (Basis.dualBasis B₂) (Basis.dualBasis B₁)) (↑Module.Dual.transpose u) i j = (↑(toMatrix B₁ B₂) u)ᵀ i j
[PROOFSTEP]
simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr, B₂.dualBasis_apply,
  Matrix.transpose_apply, LinearMap.comp_apply]
[GOAL]
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ = ↑Module.Dual.transpose (↑(toLin B₂ B₁) M)
[PROOFSTEP]
apply (LinearMap.toMatrix B₁.dualBasis B₂.dualBasis).injective
[GOAL]
case a
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module K V₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module K V₂
inst✝³ : Fintype ι₁
inst✝² : Fintype ι₂
inst✝¹ : DecidableEq ι₁
inst✝ : DecidableEq ι₂
B₁ : Basis ι₁ K V₁
B₂ : Basis ι₂ K V₂
M : Matrix ι₁ ι₂ K
⊢ ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂))
      (↑(toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) Mᵀ) =
    ↑(LinearMap.toMatrix (Basis.dualBasis B₁) (Basis.dualBasis B₂)) (↑Module.Dual.transpose (↑(toLin B₂ B₁) M))
[PROOFSTEP]
rw [LinearMap.toMatrix_toLin, LinearMap.toMatrix_transpose, LinearMap.toMatrix_toLin]


[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ IsSymm (Matrix.fromBlocks A B C D)
[PROOFSTEP]
have hCB : Cᵀ = B := by
  rw [← hBC]
  simp
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Cᵀ = B
[PROOFSTEP]
rw [← hBC]
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Bᵀᵀ = B
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ IsSymm (Matrix.fromBlocks A B C D)
[PROOFSTEP]
unfold Matrix.IsSymm
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
[PROOFSTEP]
rw [fromBlocks_transpose]
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
n : Type u_3
m : Type u_4
R : Type u_5
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
[PROOFSTEP]
rw [hA, hCB, hBC, hD]


[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      (x✝² + x✝¹) x✝ =
    (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝² x✝ +
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝¹ x✝
[PROOFSTEP]
simp only [LinearMap.map_add, add_mul]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ {
      val :=
        ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ + ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
      property :=
        (_ :
          (fun x => x ∈ even Q)
            (↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ +
              ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝)) } =
    { val := ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) } +
      { val := ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      (x✝² • x✝¹) x✝ =
    x✝² •
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝¹ x✝
[PROOFSTEP]
simp only [LinearMap.map_smul, smul_mul_assoc]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ { val := x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝),
      property := (_ : (fun x => x ∈ even Q) (x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝))) } =
    x✝² •
      { val := ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      x✝² (x✝¹ + x✝) =
    (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝² x✝¹ +
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝² x✝
[PROOFSTEP]
simp only [LinearMap.map_add, mul_add]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ {
      val :=
        ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹ +
          ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝,
      property :=
        (_ :
          (fun x => x ∈ even Q)
            (↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹ +
              ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝)) } =
    { val := ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝¹ ∈ evenOdd Q 0) } +
      { val := ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝² * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ (fun m₁ m₂ =>
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
      x✝¹ (x✝² • x✝) =
    x✝² •
      (fun m₁ m₂ =>
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ ∈ evenOdd Q 0) })
        x✝¹ x✝
[PROOFSTEP]
simp only [LinearMap.map_smul, mul_smul_comm]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² : R
x✝¹ x✝ : M
⊢ { val := x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝),
      property := (_ : (fun x => x ∈ even Q) (x✝² • (↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝))) } =
    x✝² •
      { val := ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝,
        property := (_ : ↑(CliffordAlgebra.ι Q) x✝¹ * ↑(CliffordAlgebra.ι Q) x✝ ∈ evenOdd Q 0) }
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * (↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₃) =
    ↑(CliffordAlgebra.ι Q) m₁ * (↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₃)
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ ↑(CliffordAlgebra.ι Q) m₁ * (↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₂ * ↑(CliffordAlgebra.ι Q) m₃) =
    ↑Q m₂ • (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₃)
[PROOFSTEP]
rw [Algebra.smul_def, ι_sq_scalar, Algebra.left_comm]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : EvenHom.compr₂ (ι Q) f = EvenHom.compr₂ (ι Q) g
⊢ f = g
[PROOFSTEP]
rw [EvenHom.ext_iff] at h
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
⊢ f = g
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case H.mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
[PROOFSTEP]
refine' even_induction _ _ _ _ _ hx
[GOAL]
case H.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ∀ (r : R),
    ↑f
        { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
          property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) } =
      ↑g
        { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
          property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) }
[PROOFSTEP]
intro r
[GOAL]
case H.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
r : R
⊢ ↑f
      { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) } =
    ↑g
      { val := ↑(algebraMap R (CliffordAlgebra ?m.107570)) r,
        property := (_ : ↑(algebraMap R (CliffordAlgebra ?m.107570)) r ∈ evenOdd ?m.107570 0) }
[PROOFSTEP]
exact (f.commutes r).trans (g.commutes r).symm
[GOAL]
case H.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    ↑f { val := x, property := hx } = ↑g { val := x, property := hx } →
      ↑f { val := y, property := hy } = ↑g { val := y, property := hy } →
        ↑f { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } =
          ↑g { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) }
[PROOFSTEP]
intro x y hx hy ihx ihy
[GOAL]
case H.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
ihy : ↑f { val := y, property := hy } = ↑g { val := y, property := hy }
⊢ ↑f { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } =
    ↑g { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) }
[PROOFSTEP]
have := congr_arg₂ (· + ·) ihx ihy
[GOAL]
case H.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
ihy : ↑f { val := y, property := hy } = ↑g { val := y, property := hy }
this :
  (fun x_1 x_2 => x_1 + x_2) (↑f { val := x, property := hx }) (↑f { val := y, property := hy }) =
    (fun x_1 x_2 => x_1 + x_2) (↑g { val := x, property := hx }) (↑g { val := y, property := hy })
⊢ ↑f { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } =
    ↑g { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) }
[PROOFSTEP]
exact (f.map_add _ _).trans (this.trans <| (g.map_add _ _).symm)
[GOAL]
case H.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x : CliffordAlgebra Q
hx : x ∈ even Q
⊢ ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    ↑f { val := x, property := hx } = ↑g { val := x, property := hx } →
      ↑f
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } =
        ↑g
          { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
            property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) }
[PROOFSTEP]
intro m₁ m₂ x hx ih
[GOAL]
case H.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
⊢ ↑f
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } =
    ↑g
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) }
[PROOFSTEP]
have := congr_arg₂ (· * ·) (LinearMap.congr_fun (LinearMap.congr_fun h m₁) m₂) ih
[GOAL]
case H.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ : EvenHom Q A
f g : { x // x ∈ even Q } →ₐ[R] A
h : (EvenHom.compr₂ (ι Q) f).bilin = (EvenHom.compr₂ (ι Q) g).bilin
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
ih : ↑f { val := x, property := hx } = ↑g { val := x, property := hx }
this :
  (fun x_1 x_2 => x_1 * x_2) (↑(↑(EvenHom.compr₂ (ι Q) f).bilin m₁) m₂) (↑f { val := x, property := hx }) =
    (fun x_1 x_2 => x_1 * x_2) (↑(↑(EvenHom.compr₂ (ι Q) g).bilin m₁) m₂) (↑g { val := x, property := hx })
⊢ ↑f
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } =
    ↑g
      { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
        property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) }
[PROOFSTEP]
exact (f.map_mul _ _).trans (this.trans <| (g.map_mul _ _).symm)
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
a : A × { x // x ∈ CliffordAlgebra.even.lift.S f }
m₃ : M
⊢ ↑(↑f.bilin m₃) (m₁ + m₂) * a.fst = ↑(↑f.bilin m₃) m₁ * a.fst + ↑(↑f.bilin m₃) m₂ * a.fst
[PROOFSTEP]
rw [map_add, add_mul]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
c : R
m : M
a : A × { x // x ∈ CliffordAlgebra.even.lift.S f }
m₃ : M
⊢ ↑(↑f.bilin m₃) (c • m) * a.fst = c • (↑(↑f.bilin m₃) m * a.fst)
[PROOFSTEP]
rw [LinearMap.map_smul, smul_mul_assoc]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }
⊢ ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x
[PROOFSTEP]
obtain ⟨a, ⟨g, hg⟩⟩ := x
[GOAL]
case mk.mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(↑(CliffordAlgebra.even.lift.fFold f) m)
      (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg })) =
    ↑Q m • (a, { val := g, property := hg })
[PROOFSTEP]
ext : 2
[GOAL]
case mk.mk.h₁
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ (↑(↑(CliffordAlgebra.even.lift.fFold f) m)
        (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg }))).fst =
    (↑Q m • (a, { val := g, property := hg })).fst
[PROOFSTEP]
change f.bilin m m * a = Q m • a
[GOAL]
case mk.mk.h₁
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(↑f.bilin m) m * a = ↑Q m • a
[PROOFSTEP]
rw [Algebra.smul_def, f.contract]
[GOAL]
case mk.mk.h₂.a
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
⊢ ↑(↑(↑(CliffordAlgebra.even.lift.fFold f) m)
          (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg }))).snd =
    ↑(↑Q m • (a, { val := g, property := hg })).snd
[PROOFSTEP]
ext m₁
[GOAL]
case mk.mk.h₂.a.h
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑↑(↑(↑(CliffordAlgebra.even.lift.fFold f) m)
              (↑(↑(CliffordAlgebra.even.lift.fFold f) m) (a, { val := g, property := hg }))).snd
      m₁ =
    ↑↑(↑Q m • (a, { val := g, property := hg })).snd m₁
[PROOFSTEP]
change f.bilin _ _ * g m = Q m • g m₁
[GOAL]
case mk.mk.h₂.a.h
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(↑f.bilin m₁) m * ↑g m = ↑Q m • ↑g m₁
[PROOFSTEP]
apply Submodule.span_induction' _ _ _ _ hg
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ∀ (x : M →ₗ[R] A),
    x ∈ {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
      ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁
[PROOFSTEP]
rintro _ ⟨b, m₃, rfl⟩
[GOAL]
case intro.intro
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
b : A
m₃ : M
⊢ ↑(↑f.bilin m₁) m * ↑(↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₃)) (LinearMap.mulRight R b)) m =
    ↑Q m • ↑(↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₃)) (LinearMap.mulRight R b)) m₁
[PROOFSTEP]
change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)
[GOAL]
case intro.intro
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
b : A
m₃ : M
⊢ ↑(↑f.bilin m₁) m * (↑(↑f.bilin m) m₃ * b) = ↑Q m • (↑(↑f.bilin m₁) m₃ * b)
[PROOFSTEP]
rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(↑f.bilin m₁) m * ↑0 m = ↑Q m • ↑0 m₁
[PROOFSTEP]
change
  f.bilin m₁ m * 0 =
    Q m •
      (0 : A)
        -- porting note: `•` now needs the type of `0`
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ↑(↑f.bilin m₁) m * 0 = ↑Q m • 0
[PROOFSTEP]
rw [mul_zero, smul_zero]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ∀ (x : M →ₗ[R] A),
    x ∈
        Submodule.span R
          {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
      ∀ (y : M →ₗ[R] A),
        y ∈
            Submodule.span R
              {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
          ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁ →
            ↑(↑f.bilin m₁) m * ↑y m = ↑Q m • ↑y m₁ → ↑(↑f.bilin m₁) m * ↑(x + y) m = ↑Q m • ↑(x + y) m₁
[PROOFSTEP]
rintro x hx y hy ihx ihy
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
x : M →ₗ[R] A
hx :
  x ∈
    Submodule.span R {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)}
y : M →ₗ[R] A
hy :
  y ∈
    Submodule.span R {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)}
ihx : ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁
ihy : ↑(↑f.bilin m₁) m * ↑y m = ↑Q m • ↑y m₁
⊢ ↑(↑f.bilin m₁) m * ↑(x + y) m = ↑Q m • ↑(x + y) m₁
[PROOFSTEP]
rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
⊢ ∀ (a : R) (x : M →ₗ[R] A),
    x ∈
        Submodule.span R
          {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)} →
      ↑(↑f.bilin m₁) m * ↑x m = ↑Q m • ↑x m₁ → ↑(↑f.bilin m₁) m * ↑(a • x) m = ↑Q m • ↑(a • x) m₁
[PROOFSTEP]
rintro x hx c ihx
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ CliffordAlgebra.even.lift.S f
m₁ : M
x : R
hx : M →ₗ[R] A
c :
  hx ∈
    Submodule.span R {f' | ∃ x m₂, f' = ↑(LinearMap.lcomp R A (↑(LinearMap.flip f.bilin) m₂)) (LinearMap.mulRight R x)}
ihx : ↑(↑f.bilin m₁) m * ↑hx m = ↑Q m • ↑hx m₁
⊢ ↑(↑f.bilin m₁) m * ↑(x • hx) m = ↑Q m • ↑(x • hx) m₁
[PROOFSTEP]
rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]
  -- Porting note: In Lean 3, `aux_apply` isn't a simp lemma. I changed `{ attrs := [] }` to
  -- `{ isSimp := false }`, so that `aux_apply` isn't a simp lemma.
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
⊢ { x // x ∈ even Q } →ₗ[R] A
[PROOFSTEP]
refine ?_ ∘ₗ (even Q).val.toLinearMap
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
⊢ CliffordAlgebra Q →ₗ[R] A
[PROOFSTEP]
letI : AddCommGroup (S f) := AddSubgroupClass.toAddCommGroup _
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f✝ f : EvenHom Q A
this : AddCommGroup { x // x ∈ CliffordAlgebra.even.lift.S f } :=
  AddSubgroupClass.toAddCommGroup (CliffordAlgebra.even.lift.S f)
⊢ CliffordAlgebra Q →ₗ[R] A
[PROOFSTEP]
exact LinearMap.fst R _ _ ∘ₗ foldr Q (fFold f) (fFold_fFold f) (1, 0)
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              (↑(CliffordAlgebra.ι Q) m₂)))
        (↑(CliffordAlgebra.ι Q) m₁)).fst =
    ↑(↑f.bilin m₁) m₂
[PROOFSTEP]
rw [foldr_ι, foldr_ι]
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
m₁ m₂ : M
⊢ (↑(↑(CliffordAlgebra.even.lift.fFold f) m₁) (↑(↑(CliffordAlgebra.even.lift.fFold f) m₂) (1, 0))).fst =
    ↑(↑f.bilin m₁) m₂
[PROOFSTEP]
exact mul_one _
[GOAL]
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x y : { x // x ∈ even Q }
⊢ ↑(aux f) (x * y) = ↑(aux f) x * ↑(aux f) y
[PROOFSTEP]
cases' x with x x_property
[GOAL]
case mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
y : { x // x ∈ even Q }
x : CliffordAlgebra Q
x_property : x ∈ even Q
⊢ ↑(aux f) ({ val := x, property := x_property } * y) = ↑(aux f) { val := x, property := x_property } * ↑(aux f) y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ↑(aux f) ({ val := x, property := x_property } * { val := val✝, property := property✝ }) =
    ↑(aux f) { val := x, property := x_property } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
refine' (congr_arg Prod.fst (foldr_mul _ _ _ _ _ _)).trans _
[GOAL]
case mk.mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              ↑{ val := val✝, property := property✝ }))
        ↑{ val := x, property := x_property }).fst =
    ↑(aux f) { val := x, property := x_property } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
dsimp only
[GOAL]
case mk.mk
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := x_property } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
refine' even_induction Q _ _ _ _ x_property
[GOAL]
case mk.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ∀ (r : R),
    (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                  (_ :
                    ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                      ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                        ↑Q m • x))
              (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                        (_ :
                          ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                            ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                              ↑Q m • x))
                    (1, 0))
                val✝))
          (↑(algebraMap R (CliffordAlgebra Q)) r)).fst =
      ↑(aux f)
          { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
            property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0) } *
        ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
intro r
[GOAL]
case mk.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        (↑(algebraMap R (CliffordAlgebra Q)) r)).fst =
    ↑(aux f)
        { val := ↑(algebraMap R (CliffordAlgebra Q)) r,
          property := (_ : ↑(algebraMap R (CliffordAlgebra Q)) r ∈ evenOdd Q 0) } *
      ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rw [foldr_algebraMap, aux_algebraMap]
[GOAL]
case mk.mk.refine'_1
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
r : R
⊢ (r •
        ↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                  (_ :
                    ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                      ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                        ↑Q m • x))
              (1, 0))
          val✝).fst =
    ↑(algebraMap R A) r * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
exact Algebra.smul_def r _
[GOAL]
case mk.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ∀ {x y : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0} {hy : y ∈ evenOdd Q 0},
    (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                          (_ :
                            ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                              ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                ↑Q m • x))
                      (1, 0))
                  val✝))
            x).fst =
        ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ } →
      (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                            (_ :
                              ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                                ↑(↑(CliffordAlgebra.even.lift.fFold f) m)
                                    (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                  ↑Q m • x))
                        (1, 0))
                    val✝))
              y).fst =
          ↑(aux f) { val := y, property := hy } * ↑(aux f) { val := val✝, property := property✝ } →
        (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                            (_ :
                              ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                                ↑(↑(CliffordAlgebra.even.lift.fFold f) m)
                                    (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                  ↑Q m • x))
                        (1, 0))
                    val✝))
              (x + y)).fst =
          ↑(aux f) { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } *
            ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
intro x y hx hy ihx ihy
[GOAL]
case mk.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
ihy :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        y).fst =
    ↑(aux f) { val := y, property := hy } * ↑(aux f) { val := val✝, property := property✝ }
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        (x + y)).fst =
    ↑(aux f) { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rw [LinearMap.map_add, Prod.fst_add, ihx, ihy, ← add_mul, ← LinearMap.map_add]
[GOAL]
case mk.mk.refine'_2
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
x y : CliffordAlgebra Q
hx : x ∈ evenOdd Q 0
hy : y ∈ evenOdd Q 0
ihx :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
ihy :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        y).fst =
    ↑(aux f) { val := y, property := hy } * ↑(aux f) { val := val✝, property := property✝ }
⊢ ↑(aux f) ({ val := x, property := hx } + { val := y, property := hy }) *
      ↑(aux f) { val := val✝, property := property✝ } =
    ↑(aux f) { val := x + y, property := (_ : x + y ∈ evenOdd Q 0) } * ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x : CliffordAlgebra Q
x_property : x ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
⊢ ∀ (m₁ m₂ : M) {x : CliffordAlgebra Q} {hx : x ∈ evenOdd Q 0},
    (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                          (_ :
                            ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                              ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                ↑Q m • x))
                      (1, 0))
                  val✝))
            x).fst =
        ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ } →
      (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                          (_ :
                            ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                              ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                                ↑Q m • x))
                      (1, 0))
                  val✝))
            (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x)).fst =
        ↑(aux f)
            { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
              property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } *
          ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rintro m₁ m₂ x (hx : x ∈ even Q) ih
[GOAL]
case mk.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ even Q
ih :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
⊢ (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        (↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x)).fst =
    ↑(aux f)
        { val := ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x,
          property := (_ : ↑(CliffordAlgebra.ι Q) m₁ * ↑(CliffordAlgebra.ι Q) m₂ * x ∈ evenOdd Q 0) } *
      ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rw [aux_apply, foldr_mul, foldr_mul, foldr_ι, foldr_ι, fst_fFold_fFold, ih, ← mul_assoc, Subtype.coe_mk, foldr_mul,
  foldr_mul, foldr_ι, foldr_ι, fst_fFold_fFold]
[GOAL]
case mk.mk.refine'_3
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type uA
B : Type uB
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : EvenHom Q A
x✝ : CliffordAlgebra Q
x_property : x✝ ∈ even Q
val✝ : CliffordAlgebra Q
property✝ : val✝ ∈ even Q
m₁ m₂ : M
x : CliffordAlgebra Q
hx : x ∈ even Q
ih :
  (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                (_ :
                  ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                    ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) = ↑Q m • x))
            (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                      (_ :
                        ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                          ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                            ↑Q m • x))
                  (1, 0))
              val✝))
        x).fst =
    ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ }
⊢ ↑(↑f.bilin m₁) m₂ * ↑(aux f) { val := x, property := hx } * ↑(aux f) { val := val✝, property := property✝ } =
    ↑(↑f.bilin m₁) m₂ *
        (↑(↑(foldr Q (CliffordAlgebra.even.lift.fFold f)
                    (_ :
                      ∀ (m : M) (x : A × { x // x ∈ CliffordAlgebra.even.lift.S f }),
                        ↑(↑(CliffordAlgebra.even.lift.fFold f) m) (↑(↑(CliffordAlgebra.even.lift.fFold f) m) x) =
                          ↑Q m • x))
                (1, 0))
            x).fst *
      ↑(aux f) { val := val✝, property := property✝ }
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
⊢ (∀ (i j : n), star (A j i) = A i j) → IsHermitian A
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ IsHermitian A
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j
[PROOFSTEP]
exact h i j
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ IsHermitian Aᵀ
[PROOFSTEP]
rw [IsHermitian, conjTranspose, transpose_map]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ (Matrix.map Aᵀ star)ᵀ = Aᵀ
[PROOFSTEP]
exact congr_arg Matrix.transpose h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
⊢ IsHermitian Aᵀ → IsHermitian A
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian A
[PROOFSTEP]
rw [← transpose_transpose A]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian Aᵀᵀ
[PROOFSTEP]
exact IsHermitian.transpose h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
e : m ≃ n
h : IsHermitian (submatrix A ↑e ↑e)
⊢ IsHermitian A
[PROOFSTEP]
simpa using h.submatrix e.symm
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
⊢ IsHermitian (Matrix.fromBlocks A B C D)
[PROOFSTEP]
have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
⊢ Cᴴ = B
[PROOFSTEP]
rw [← hBC, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ IsHermitian (Matrix.fromBlocks A B C D)
[PROOFSTEP]
unfold Matrix.IsHermitian
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
[PROOFSTEP]
rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype n
A : Matrix m n α
⊢ IsHermitian (A * Aᴴ)
[PROOFSTEP]
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m n α
⊢ IsHermitian (Aᴴ * A)
[PROOFSTEP]
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m m α
B : Matrix m n α
hA : IsHermitian A
⊢ IsHermitian (Bᴴ * A * B)
[PROOFSTEP]
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m m α
B : Matrix n m α
hA : IsHermitian A
⊢ IsHermitian (B * A * Bᴴ)
[PROOFSTEP]
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : IsHermitian A
⊢ IsHermitian A⁻¹
[PROOFSTEP]
simp [IsHermitian, conjTranspose_nonsing_inv, hA.eq]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A
[PROOFSTEP]
rw [← inv_inv_of_invertible A]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A⁻¹⁻¹
[PROOFSTEP]
exact IsHermitian.inv h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : IsHermitian A
⊢ IsHermitian (Matrix.adjugate A)
[PROOFSTEP]
simp [IsHermitian, adjugate_conjTranspose, hA.eq]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : IsROrC α
inst✝ : IsROrC β
A : Matrix n n α
h : IsHermitian A
i : n
⊢ ↑(↑re (A i i)) = A i i
[PROOFSTEP]
rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ LinearMap.IsSymmetric (↑toEuclideanLin A)
[PROOFSTEP]
rw [LinearMap.IsSymmetric, (PiLp.equiv 2 fun _ : n => α).symm.surjective.forall₂]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔
    ∀ (x₁ x₂ : n → α),
      inner (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₁)) (↑(PiLp.equiv 2 fun x => α).symm x₂) =
        inner (↑(PiLp.equiv 2 fun x => α).symm x₁) (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₂))
[PROOFSTEP]
simp only [toEuclideanLin_piLp_equiv_symm, EuclideanSpace.inner_piLp_equiv_symm, toLin'_apply, star_mulVec,
  dotProduct_mulVec]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A → ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
[PROOFSTEP]
rintro (h : Aᴴ = A) x y
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : Aᴴ = A
x y : n → α
⊢ vecMul (star x) Aᴴ ⬝ᵥ y = vecMul (star x) A ⬝ᵥ y
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ (∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂) → IsHermitian A
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
⊢ IsHermitian A
[PROOFSTEP]
ext i j
[GOAL]
case mpr.a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
i j : n
⊢ Aᴴ i j = A i j
[PROOFSTEP]
simpa only [(Pi.single_star i 1).symm, ← star_mulVec, mul_one, dotProduct_single, single_vecMul, star_one,
  one_mul] using h (Pi.single i 1) (Pi.single j 1)


[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
⊢ Nondegenerate M
[PROOFSTEP]
intro v hv
[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
[PROOFSTEP]
ext i
[GOAL]
case h
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : ∀ (w : m → A), v ⬝ᵥ mulVec M w = 0
i : m
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
specialize hv (M.cramer (Pi.single i 1))
[GOAL]
case h
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
refine' (mul_eq_zero.mp _).resolve_right hM
[GOAL]
case h
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = 0
[PROOFSTEP]
convert hv
[GOAL]
case h.e'_2
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1))
[PROOFSTEP]
simp only [mulVec_cramer M (Pi.single i 1), dotProduct, Pi.smul_apply, smul_eq_mul]
[GOAL]
case h.e'_2
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ v i * det M = Finset.sum Finset.univ fun x => v x * (det M * Pi.single i 1 x)
[PROOFSTEP]
rw [Finset.sum_eq_single i, Pi.single_eq_same, mul_one]
[GOAL]
case h.e'_2.h₀
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ i → v b * (det M * Pi.single i 1 b) = 0
[PROOFSTEP]
intro j _ hj
[GOAL]
case h.e'_2.h₀
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
j : m
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ v j * (det M * Pi.single i 1 j) = 0
[PROOFSTEP]
simp [hj]
[GOAL]
case h.e'_2.h₁
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
⊢ ¬i ∈ Finset.univ → v i * (det M * Pi.single i 1 i) = 0
[PROOFSTEP]
intros
[GOAL]
case h.e'_2.h₁
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
[PROOFSTEP]
have := Finset.mem_univ i
[GOAL]
case h.e'_2.h₁
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
i : m
hv : v ⬝ᵥ mulVec M (↑(cramer M) (Pi.single i 1)) = 0
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ v i * (det M * Pi.single i 1 i) = 0
[PROOFSTEP]
contradiction
[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : vecMul v M = 0
w : m → A
⊢ v ⬝ᵥ mulVec M w = 0
[PROOFSTEP]
rw [dotProduct_mulVec, hv, zero_dotProduct]
[GOAL]
m : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDomain A
inst✝ : DecidableEq m
M : Matrix m m A
hM : det M ≠ 0
v : m → A
hv : mulVec M v = 0
⊢ det Mᵀ ≠ 0
[PROOFSTEP]
rwa [det_transpose]