[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix b b) f) = trace (↑(toMatrix b b) (comp (comp id f) id))
[PROOFSTEP]
rw [LinearMap.id_comp, LinearMap.comp_id]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix b b) (comp (comp id f) id)) = trace (↑(toMatrix c b) id * ↑(toMatrix c c) f * ↑(toMatrix b c) id)
[PROOFSTEP]
rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c b) id * ↑(toMatrix c c) f * ↑(toMatrix b c) id) =
    trace (↑(toMatrix c c) f * ↑(toMatrix b c) id * ↑(toMatrix c b) id)
[PROOFSTEP]
rw [Matrix.mul_assoc, Matrix.trace_mul_comm]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c c) f * ↑(toMatrix b c) id * ↑(toMatrix c b) id) = trace (↑(toMatrix c c) (comp (comp f id) id))
[PROOFSTEP]
rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ trace (↑(toMatrix c c) (comp (comp f id) id)) = trace (↑(toMatrix c c) f)
[PROOFSTEP]
rw [LinearMap.comp_id, LinearMap.comp_id]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
⊢ ↑(trace R M) f = Matrix.trace (↑(toMatrix b b) f)
[PROOFSTEP]
have : ∃ s : Finset M, Nonempty (Basis s R M) := ⟨s, ⟨b⟩⟩
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) f = Matrix.trace (↑(toMatrix b b) f)
[PROOFSTEP]
rw [trace, dif_pos this, ← traceAux_def]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(traceAux R (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose this } R M)))) f = ↑(traceAux R b) f
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
s : Finset M
b : Basis { x // x ∈ s } R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ traceAux R (Nonempty.some (_ : Nonempty (Basis { x // x ∈ Exists.choose this } R M))) = traceAux R b
[PROOFSTEP]
apply traceAux_eq
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ↑(trace R M) f = Matrix.trace (↑(toMatrix b b) f)
[PROOFSTEP]
rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
  traceAux_eq R b b.reindexFinsetRange]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
[PROOFSTEP]
let ⟨s, ⟨b⟩⟩ := H
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
[PROOFSTEP]
simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b✝ : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ Matrix.trace (↑(toMatrix b b) f * ↑(toMatrix b b) g) = Matrix.trace (↑(toMatrix b b) g * ↑(toMatrix b b) f)
[PROOFSTEP]
apply Matrix.trace_mul_comm
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ ↑(trace R M) (f * g) = ↑(trace R M) (g * f)
[PROOFSTEP]
rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g h : M →ₗ[R] M
⊢ ↑(trace R M) (f * g * h) = ↑(trace R M) (h * f * g)
[PROOFSTEP]
rw [LinearMap.trace_mul_comm, ← mul_assoc]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f g h : M →ₗ[R] M
⊢ ↑(trace R M) (f * (g * h)) = ↑(trace R M) (h * (f * g))
[PROOFSTEP]
rw [← mul_assoc, LinearMap.trace_mul_comm]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ ↑(trace R M) (↑f * g * ↑f⁻¹) = ↑(trace R M) g
[PROOFSTEP]
rw [trace_mul_comm]
[GOAL]
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ ↑(trace R M) (↑f⁻¹ * (↑f * g)) = ↑(trace R M) g
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
[PROOFSTEP]
classical
cases nonempty_fintype ι
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
rintro ⟨i, j⟩
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
by_cases hij : i = j
· rw [hij]
  simp
rw [Matrix.StdBasisMatrix.trace_zero j i (1 : R) hij]
simp [Finsupp.single_eq_pi_single, hij]
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
[PROOFSTEP]
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
[GOAL]
case intro
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i) =
      ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i)
[PROOFSTEP]
rintro ⟨i, j⟩
[GOAL]
case intro.mk
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j)) =
    ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j))
[PROOFSTEP]
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
[GOAL]
case intro.mk
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(trace R M) (↑(dualTensorHom R M M) (Basis.coord b i ⊗ₜ[R] ↑b j)) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
[GOAL]
case intro.mk
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
rw [hij]
[GOAL]
case pos
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j j 1) = ↑(contractLeft R M) (Basis.coord b j ⊗ₜ[R] ↑b j)
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
rw [Matrix.StdBasisMatrix.trace_zero j i (1 : R) hij]
[GOAL]
case neg
R : Type u_1
inst✝⁷ : CommRing R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup P
inst✝¹ : Module R P
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ 0 = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
[PROOFSTEP]
simp [Finsupp.single_eq_pi_single, hij]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R M
⊢ trace R M = comp (contractLeft R M) ↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b))
[PROOFSTEP]
simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
x : Module.Dual R M ⊗[R] M
⊢ ↑(trace R M) (↑(dualTensorHom R M M) x) = ↑(contractLeft R M) x
[PROOFSTEP]
rw [← comp_apply, trace_eq_contract]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Subsingleton R
⊢ ↑(trace R M) 1 = ↑(finrank R M)
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
have b := Module.Free.chooseBasis R M
[GOAL]
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R M) R M
⊢ ↑(trace R M) 1 = ↑(finrank R M)
[PROOFSTEP]
rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]
[GOAL]
case inr
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(Fintype.card (Module.Free.ChooseBasisIndex R M))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ ↑(trace R M) id = ↑(finrank R M)
[PROOFSTEP]
rw [← one_eq_id, trace_one]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
[PROOFSTEP]
let e := dualTensorHomEquiv R M M
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
[PROOFSTEP]
have h : Function.Surjective e.toLinearMap := e.surjective
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
[PROOFSTEP]
refine' (cancel_right h).1 _
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e = comp (trace R M) ↑e
[PROOFSTEP]
ext f m
[GOAL]
case a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
f : Module.Dual R M
m : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e)) f) m =
    ↑(↑(AlgebraTensorModule.curry (comp (trace R M) ↑e)) f) m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ comp (trace R (M × N)) (prodMapLinear R M N M N R) = comp (coprod id id) (prodMap (trace R M) (trace R N))
[PROOFSTEP]
let e := (dualTensorHomEquiv R M M).prod (dualTensorHomEquiv R N N)
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
⊢ comp (trace R (M × N)) (prodMapLinear R M N M N R) = comp (coprod id id) (prodMap (trace R M) (trace R N))
[PROOFSTEP]
have h : Function.Surjective e.toLinearMap := e.surjective
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
⊢ comp (trace R (M × N)) (prodMapLinear R M N M N R) = comp (coprod id id) (prodMap (trace R M) (trace R N))
[PROOFSTEP]
refine' (cancel_right h).1 _
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
⊢ comp (comp (trace R (M × N)) (prodMapLinear R M N M N R)) ↑e =
    comp (comp (coprod id id) (prodMap (trace R M) (trace R N))) ↑e
[PROOFSTEP]
ext
[GOAL]
case hl.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
x✝¹ : Module.Dual R M
x✝ : M
⊢ ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (trace R (M × N)) (prodMapLinear R M N M N R)) ↑e)
                (inl R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝ =
    ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (coprod id id) (prodMap (trace R M) (trace R N))) ↑e)
                (inl R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [dualTensorHomEquiv, LinearEquiv.coe_prod, dualTensorHomEquivOfBasis_toLinearMap,
  AlgebraTensorModule.curry_apply, curry_apply, coe_restrictScalars, coe_comp, coe_inl, Function.comp_apply,
  prodMap_apply, map_zero, prodMapLinear_apply, dualTensorHom_prodMap_zero, trace_eq_contract_apply, contractLeft_apply,
  fst_apply, coprod_apply, id_coe, id_eq, add_zero]
[GOAL]
case hr.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
e : (Module.Dual R M ⊗[R] M × Module.Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  LinearEquiv.prod (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h : Function.Surjective ↑↑e
x✝¹ : Module.Dual R N
x✝ : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (trace R (M × N)) (prodMapLinear R M N M N R)) ↑e)
                (inr R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝ =
    ↑(↑(AlgebraTensorModule.curry
              (comp (comp (comp (coprod id id) (prodMap (trace R M) (trace R N))) ↑e)
                (inr R (Module.Dual R M ⊗[R] M) (Module.Dual R N ⊗[R] N))))
          x✝¹)
      x✝
[PROOFSTEP]
simp only [dualTensorHomEquiv, LinearEquiv.coe_prod, dualTensorHomEquivOfBasis_toLinearMap,
  AlgebraTensorModule.curry_apply, curry_apply, coe_restrictScalars, coe_comp, coe_inr, Function.comp_apply,
  prodMap_apply, map_zero, prodMapLinear_apply, zero_prodMap_dualTensorHom, trace_eq_contract_apply, contractLeft_apply,
  snd_apply, coprod_apply, id_coe, id_eq, zero_add]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
[PROOFSTEP]
have h := ext_iff.1 (trace_prodMap R M N) (f, g)
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  ↑(comp (trace R (M × N)) (prodMapLinear R M N M N R)) (f, g) =
    ↑(comp (coprod id id) (prodMap (trace R M) (trace R N))) (f, g)
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, prodMap_apply, coprod_apply, id_coe, id.def, prodMapLinear_apply] at h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h : ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N)) = compl₁₂ (lsmul R R) (trace R M) (trace R N)
[PROOFSTEP]
apply
  (compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective)
      (show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).1
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compl₁₂ (compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M) (dualTensorHom R N N) =
    compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N)
[PROOFSTEP]
ext f m g n
[GOAL]
case a.h.h.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : Module.Dual R M
m : M
g : Module.Dual R N
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n
[PROOFSTEP]
simp only [AlgebraTensorModule.curry_apply, toFun_eq_coe, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply,
  compr₂_apply, mapBilinear_apply, trace_eq_contract_apply, contractLeft_apply, lsmul_apply, Algebra.id.smul_eq_mul,
  map_dualTensorHom, dualDistrib_apply]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compr₂ (llcomp R M N M) (trace R M) = compr₂ (flip (llcomp R N M N)) (trace R N)
[PROOFSTEP]
apply
  (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
      (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
⊢ compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N) =
    compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N)
[PROOFSTEP]
ext g m f n
[GOAL]
case a.h.h.a.h.h
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
g : Module.Dual R N
m : M
f : Module.Dual R M
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N)))
                    g)
                m))
          f)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                          (dualTensorHom R M N)))
                    g)
                m))
          f)
      n
[PROOFSTEP]
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply, compr₂_apply,
  llcomp_apply', comp_dualTensorHom, map_smulₛₗ, RingHom.id_apply, trace_eq_contract_apply, contractLeft_apply,
  smul_eq_mul, mul_comm, flip_apply]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
⊢ ↑(trace R (Module.Dual R M)) (↑Module.Dual.transpose f) = ↑(trace R M) f
[PROOFSTEP]
rw [← comp_apply, trace_transpose]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
[PROOFSTEP]
have h := ext_iff.1 (ext_iff.1 (trace_tensorProduct R M N) f) g
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  ↑(↑(compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) f) g = ↑(↑(compl₁₂ (lsmul R R) (trace R M) (trace R N)) f) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
[PROOFSTEP]
simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply, Algebra.id.smul_eq_mul] at h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
g : N →ₗ[R] N
h : ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
[PROOFSTEP]
have h := ext_iff.1 (ext_iff.1 (trace_comp_comm R M N) g) f
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(↑(compr₂ (llcomp R M N M) (trace R M)) g) f = ↑(↑(compr₂ (flip (llcomp R N M N)) (trace R N)) g) f
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
[PROOFSTEP]
simp only [llcomp_apply', compr₂_apply, flip_apply] at h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] M
h : ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
⊢ ↑(trace R M) (comp g f) = ↑(trace R N) (comp f g)
[PROOFSTEP]
exact h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ ↑(trace R P) (comp g (comp f h)) = ↑(trace R N) (comp f (comp h g))
[PROOFSTEP]
rw [trace_comp_comm', comp_assoc]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ ↑(trace R P) (comp (comp g f) h) = ↑(trace R M) (comp (comp h g) f)
[PROOFSTEP]
rw [trace_comp_comm', ← comp_assoc]
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Type u_2
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_3
P : Type u_4
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
inst✝⁷ : AddCommGroup P
inst✝⁶ : Module R P
ι : Type u_5
inst✝⁵ : Module.Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Free R N
inst✝² : Module.Finite R N
inst✝¹ : Module.Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ ↑(trace R N) (↑(LinearEquiv.conj e) f) = ↑(trace R M) f
[PROOFSTEP]
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm,
  LinearEquiv.refl_toLinearMap, id_comp]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
M : Type u_2
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
inst✝¹¹ : AddCommGroup P
inst✝¹⁰ : Module R P
ι : Type u_5
inst✝⁹ : Module.Free R M
inst✝⁸ : Module.Finite R M
inst✝⁷ : Module.Free R N
inst✝⁶ : Module.Finite R N
inst✝⁵ : Module.Free R P
inst✝⁴ : Module.Finite R P
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Module.Free R { x // x ∈ p }
inst✝² : Module.Finite R { x // x ∈ p }
inst✝¹ : Module.Free R { x // x ∈ ker f }
inst✝ : Module.Finite R { x // x ∈ ker f }
⊢ ↑(LinearMap.trace R M) f = ↑(finrank R { x // x ∈ p })
[PROOFSTEP]
rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]


[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let A := toMatrix b b f
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let b' := chooseBasis R M
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let ι' := ChooseBasisIndex R M
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let A' := toMatrix b' b' f
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let e := Basis.indexEquiv b b'
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ := reindexLinearEquiv R R e e
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ₁ := reindexLinearEquiv R R e (Equiv.refl ι')
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ₂ := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let φ₃ := reindexLinearEquiv R R (Equiv.refl ι') e
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let P := b.toMatrix b'
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
let Q := b'.toMatrix b
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
have hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1 := by
  rw [RingHom.mapMatrix_apply, RingHom.mapMatrix_apply, ← Matrix.map_mul, reindexLinearEquiv_mul R R,
    Basis.toMatrix_mul_toMatrix_flip, reindexLinearEquiv_one, ← RingHom.mapMatrix_apply, RingHom.map_one]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
[PROOFSTEP]
rw [RingHom.mapMatrix_apply, RingHom.mapMatrix_apply, ← Matrix.map_mul, reindexLinearEquiv_mul R R,
  Basis.toMatrix_mul_toMatrix_flip, reindexLinearEquiv_one, ← RingHom.mapMatrix_apply, RingHom.map_one]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
[PROOFSTEP]
calc
  A.charpoly = (reindex e e A).charpoly := (charpoly_reindex _ _).symm
  _ = det (scalar ι' X - C.mapMatrix (φ A)) := rfl
  _ = det (scalar ι' X - C.mapMatrix (φ (P * A' * Q))) := by
    rw [basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix]
  _ = det (scalar ι' X - C.mapMatrix (φ₁ P * φ₂ A' * φ₃ Q)) := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
  _ = det (scalar ι' X - C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)) := by simp
  _ =
      det
        (scalar ι' X * C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) -
          C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)) :=
    by rw [Matrix.mul_assoc ((scalar ι') X), hPQ, Matrix.mul_one]
  _ =
      det
        (C.mapMatrix (φ₁ P) * scalar ι' X * C.mapMatrix (φ₃ Q) -
          C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)) :=
    by simp
  _ = det (C.mapMatrix (φ₁ P) * (scalar ι' X - C.mapMatrix A') * C.mapMatrix (φ₃ Q)) := by
    rw [← Matrix.sub_mul, ← Matrix.mul_sub]
  _ = det (C.mapMatrix (φ₁ P)) * det (scalar ι' X - C.mapMatrix A') * det (C.mapMatrix (φ₃ Q)) := by
    rw [det_mul, det_mul]
  _ = det (C.mapMatrix (φ₁ P)) * det (C.mapMatrix (φ₃ Q)) * det (scalar ι' X - C.mapMatrix A') := by ring
  _ = det (scalar ι' X - C.mapMatrix A') := by rw [← det_mul, hPQ, det_one, one_mul]
  _ = f.charpoly := rfl
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ A)) = det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ (P * A' * Q)))
[PROOFSTEP]
rw [basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ (P * A' * Q))) =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P * ↑φ₂ A' * ↑φ₃ Q))
[PROOFSTEP]
rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P * ↑φ₂ A' * ↑φ₃ Q)) =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
simp
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det
      (↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
rw [Matrix.mul_assoc ((scalar ι') X), hPQ, Matrix.mul_one]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det
      (↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det
      (↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
simp
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det
      (↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(scalar ι') X * ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) A' * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P) * (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') * ↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
rw [← Matrix.sub_mul, ← Matrix.mul_sub]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P) * (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') * ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') *
      det (↑(RingHom.mapMatrix C) (↑φ₃ Q))
[PROOFSTEP]
rw [det_mul, det_mul]
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') *
      det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) *
      det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A')
[PROOFSTEP]
ring
[GOAL]
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) * ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) *
      det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A')
[PROOFSTEP]
rw [← det_mul, hPQ, det_one, one_mul]


[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f g : IsometryEquiv Q₁ Q₂
⊢ (fun f => ↑f.toLinearEquiv) f = (fun f => ↑f.toLinearEquiv) g →
    (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) f = (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) g → f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
g : IsometryEquiv Q₁ Q₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), ↑Q₂ (AddHom.toFun toLinearEquiv✝.toAddHom m) = ↑Q₁ m
⊢ (fun f => ↑f.toLinearEquiv) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } =
      (fun f => ↑f.toLinearEquiv) g →
    (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } =
        (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) g →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
toLinearEquiv✝¹ : M₁ ≃ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), ↑Q₂ (AddHom.toFun toLinearEquiv✝¹.toAddHom m) = ↑Q₁ m
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), ↑Q₂ (AddHom.toFun toLinearEquiv✝.toAddHom m) = ↑Q₁ m
⊢ (fun f => ↑f.toLinearEquiv) { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
      (fun f => ↑f.toLinearEquiv) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } →
    (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        (fun f => ↑(LinearEquiv.symm f.toLinearEquiv)) { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } →
      { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
⊢ ∀ (m : M₂),
    ↑Q₁
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m) =
      ↑Q₂ m
[PROOFSTEP]
intro m
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
m : M₂
⊢ ↑Q₁
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    ↑Q₂ m
[PROOFSTEP]
rw [← f.map_app]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
m : M₂
⊢ ↑Q₂
      (↑f
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m)) =
    ↑Q₂ m
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
src✝ : M₂ ≃ₗ[R] M₁ := LinearEquiv.symm f.toLinearEquiv
m : M₂
⊢ ↑f
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    m
[PROOFSTEP]
exact f.toLinearEquiv.apply_symm_apply m
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
g : IsometryEquiv Q₂ Q₃
src✝ : M₁ ≃ₗ[R] M₃ := LinearEquiv.trans f.toLinearEquiv g.toLinearEquiv
⊢ ∀ (m : M₁),
    ↑Q₃
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m) =
      ↑Q₁ m
[PROOFSTEP]
intro m
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
g : IsometryEquiv Q₂ Q₃
src✝ : M₁ ≃ₗ[R] M₃ := LinearEquiv.trans f.toLinearEquiv g.toLinearEquiv
m : M₁
⊢ ↑Q₃
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    ↑Q₁ m
[PROOFSTEP]
rw [← f.map_app, ← g.map_app]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : IsometryEquiv Q₁ Q₂
g : IsometryEquiv Q₂ Q₃
src✝ : M₁ ≃ₗ[R] M₃ := LinearEquiv.trans f.toLinearEquiv g.toLinearEquiv
m : M₁
⊢ ↑Q₃
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m) =
    ↑Q₃ (↑g (↑f m))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
f : M₁ ≃ₗ[R] M
src✝ : M ≃ₗ[R] M₁ := LinearEquiv.symm f
⊢ ∀ (m : M),
    ↑(comp Q ↑f)
        (AddHom.toFun
          (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun,
                left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
          m) =
      ↑Q m
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
f : M₁ ≃ₗ[R] M
src✝ : M ≃ₗ[R] M₁ := LinearEquiv.symm f
m✝ : M
⊢ ↑(comp Q ↑f)
      (AddHom.toFun
        (↑{ toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }).toAddHom
        m✝) =
    ↑Q m✝
[PROOFSTEP]
simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe, LinearEquiv.apply_symm_apply, f.apply_symm_apply]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
⊢ IsometryEquiv Q (weightedSumSquares K fun i => ↑Q (↑v i))
[PROOFSTEP]
let iso := Q.isometryEquivBasisRepr v
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
⊢ IsometryEquiv Q (weightedSumSquares K fun i => ↑Q (↑v i))
[PROOFSTEP]
refine' ⟨iso, fun m => _⟩
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ ↑(weightedSumSquares K fun i => ↑Q (↑v i)) (AddHom.toFun iso.toAddHom m) = ↑Q m
[PROOFSTEP]
convert iso.map_app m
[GOAL]
case h.e'_2.h.e'_5
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹³ : Semiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Fintype ι
v✝ : Basis ι R M
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : BilinForm.iIsOrtho (↑associated Q) ↑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ (weightedSumSquares K fun i => ↑Q (↑v i)) = basisRepr Q v
[PROOFSTEP]
rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]
[GOAL]
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
[GOAL]
case intro
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v✝ : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : iIsOrtho (↑(associatedHom K) Q) ↑v
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
have hv₂ := hv₁.not_isOrtho_basis_self_of_nondegenerate hQ
[GOAL]
case intro
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v✝ : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : iIsOrtho (↑(associatedHom K) Q) ↑v
hv₂ : ∀ (i : Fin (FiniteDimensional.finrank K V)), ¬IsOrtho (↑(associatedHom K) Q) (↑v i) (↑v i)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
simp_rw [IsOrtho, associated_eq_self_apply] at hv₂
[GOAL]
case intro
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : Module R M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : Fintype ι
v✝ : Basis ι R M
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : Nondegenerate (↑associated Q)
v : Basis (Fin (FiniteDimensional.finrank K V)) K V
hv₁ : iIsOrtho (↑(associatedHom K) Q) ↑v
hv₂ : ∀ (i : Fin (FiniteDimensional.finrank K V)), ¬↑Q (↑v i) = 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
[PROOFSTEP]
exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩


[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
⊢ IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1)
[PROOFSTEP]
let w i := if h : w' i = 0 then (1 : Units ℂ) else Units.mk0 (w' i) h
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
⊢ IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1)
[PROOFSTEP]
have hw' : ∀ i : ι, (w i : ℂ) ^ (-(1 / 2 : ℂ)) ≠ 0 := by
  intro i hi
  exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
⊢ ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
i : ι
hi : ↑(w i) ^ (-(1 / 2)) = 0
⊢ False
[PROOFSTEP]
exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
⊢ IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1)
[PROOFSTEP]
convert
  (weightedSumSquares ℂ w').isometryEquivBasisRepr
    ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit)
[GOAL]
case h.e'_10
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
⊢ (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1) =
    basisRepr (weightedSumSquares ℂ w')
      (Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2)))))
[PROOFSTEP]
ext1 v
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
⊢ ↑(weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1) v =
    ↑(basisRepr (weightedSumSquares ℂ w')
          (Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))))
      v
[PROOFSTEP]
erw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
⊢ ∑ i : ι, (if w' i = 0 then 0 else 1) • (v i * v i) =
    ∑ i : ι,
      w' i •
        (Finset.sum univ
            (fun i =>
              v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
            i *
          Finset.sum univ
            (fun i =>
              v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
            i)
[PROOFSTEP]
refine' sum_congr rfl fun j hj => _
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ (if w' j = 0 then 0 else 1) • (v j * v j) =
    w' j •
      (Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j *
        Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j)
[PROOFSTEP]
have hsum :
  (∑ i : ι, v i • ((isUnit_iff_ne_zero.2 <| hw' i).unit : ℂ) • (Pi.basisFun ℂ ι) i) j = v j • w j ^ (-(1 / 2 : ℂ)) :=
  by
  rw [Finset.sum_apply, sum_eq_single j, Pi.basisFun_apply, IsUnit.unit_spec, LinearMap.stdBasis_apply, Pi.smul_apply,
    Pi.smul_apply, Function.update_same, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_one]
  intro i _ hij
  rw [Pi.basisFun_apply, LinearMap.stdBasis_apply, Pi.smul_apply, Pi.smul_apply, Function.update_noteq hij.symm,
    Pi.zero_apply, smul_eq_mul, smul_eq_mul, mul_zero, mul_zero]
  intro hj'; exact False.elim (hj' hj)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
[PROOFSTEP]
rw [Finset.sum_apply, sum_eq_single j, Pi.basisFun_apply, IsUnit.unit_spec, LinearMap.stdBasis_apply, Pi.smul_apply,
  Pi.smul_apply, Function.update_same, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_one]
[GOAL]
case h₀
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ∀ (b : ι), b ∈ univ → b ≠ j → (v b • ↑(IsUnit.unit (_ : IsUnit (↑(w b) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) b) j = 0
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w j) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) j) j = 0
[PROOFSTEP]
intro i _ hij
[GOAL]
case h₀
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
i : ι
a✝ : i ∈ univ
hij : i ≠ j
⊢ (v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j = 0
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w j) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) j) j = 0
[PROOFSTEP]
rw [Pi.basisFun_apply, LinearMap.stdBasis_apply, Pi.smul_apply, Pi.smul_apply, Function.update_noteq hij.symm,
  Pi.zero_apply, smul_eq_mul, smul_eq_mul, mul_zero, mul_zero]
[GOAL]
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w j) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) j) j = 0
[PROOFSTEP]
intro hj'
[GOAL]
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hj' : ¬j ∈ univ
⊢ (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w j) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) j) j = 0
[PROOFSTEP]
exact False.elim (hj' hj)
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
⊢ (if w' j = 0 then 0 else 1) • (v j * v j) =
    w' j •
      (Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j *
        Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j)
[PROOFSTEP]
simp_rw [Basis.unitsSMul_apply]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
⊢ (if w' j = 0 then 0 else 1) • (v j * v j) =
    w' j •
      (Finset.sum univ (fun x => v x • IsUnit.unit (_ : IsUnit (↑(w x) ^ (-(1 / 2)))) • ↑(Pi.basisFun ℂ ι) x) j *
        Finset.sum univ (fun x => v x • IsUnit.unit (_ : IsUnit (↑(w x) ^ (-(1 / 2)))) • ↑(Pi.basisFun ℂ ι) x) j)
[PROOFSTEP]
erw [hsum, smul_eq_mul]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
⊢ (if w' j = 0 then 0 else 1) * (v j * v j) = w' j • (v j • ↑(w j) ^ (-(1 / 2)) * v j • ↑(w j) ^ (-(1 / 2)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : w' j = 0
⊢ 0 * (v j * v j) = w' j • (v j • ↑1 ^ (-(1 / 2)) * v j • ↑1 ^ (-(1 / 2)))
[PROOFSTEP]
simp only [h, zero_smul, zero_mul]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
⊢ 1 * (v j * v j) = w' j • (v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)) * v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)))
[PROOFSTEP]
have hww' : w' j = w j := by simp only [dif_neg h, Units.val_mk0]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
⊢ w' j = ↑(w j)
[PROOFSTEP]
simp only [dif_neg h, Units.val_mk0]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ 1 * (v j * v j) = w' j • (v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)) * v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)))
[PROOFSTEP]
simp only [one_mul, Units.val_mk0, smul_eq_mul]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ v j * v j = w' j * (v j * w' j ^ (-(1 / 2)) * (v j * w' j ^ (-(1 / 2))))
[PROOFSTEP]
rw [hww']
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ v j * v j = ↑(w j) * (v j * ↑(w j) ^ (-(1 / 2)) * (v j * ↑(w j) ^ (-(1 / 2))))
[PROOFSTEP]
suffices v j * v j = w j ^ (-(1 / 2 : ℂ)) * w j ^ (-(1 / 2 : ℂ)) * w j * v j * v j by rw [this]; ring
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
this : v j * v j = ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j
⊢ v j * v j = ↑(w j) * (v j * ↑(w j) ^ (-(1 / 2)) * (v j * ↑(w j) ^ (-(1 / 2))))
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
this : v j * v j = ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j
⊢ ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j =
    ↑(w j) * (v j * ↑(w j) ^ (-(1 / 2)) * (v j * ↑(w j) ^ (-(1 / 2))))
[PROOFSTEP]
ring
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ v j * v j = ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j
[PROOFSTEP]
rw [← Complex.cpow_add _ _ (w j).ne_zero, show -(1 / 2 : ℂ) + -(1 / 2) = -1 by simp [← two_mul], Complex.cpow_neg_one,
  inv_mul_cancel (w j).ne_zero, one_mul]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ -(1 / 2) + -(1 / 2) = -1
[PROOFSTEP]
simp [← two_mul]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℂˣ
⊢ IsometryEquiv (weightedSumSquares ℂ w) (weightedSumSquares ℂ 1)
[PROOFSTEP]
simpa using isometryEquivSumSquares ((↑) ∘ w)


[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
⊢ ↑LinearMap.det 0 = 0
[PROOFSTEP]
letI : Nonempty (Module.Free.ChooseBasisIndex R M) := (Module.Free.chooseBasis R M).index_nonempty
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
⊢ ↑LinearMap.det 0 = 0
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
this : Nonempty (Module.Free.ChooseBasisIndex R M) := Basis.index_nonempty (Module.Free.chooseBasis R M)
✝ : Nontrivial R
⊢ ↑LinearMap.det 0 = 0
[PROOFSTEP]
exact LinearMap.det_zero' (Module.Free.chooseBasis R M)