-- Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean
@[simp]
lemma LinearEquiv.charpoly_conj (e : M₁ ≃ₗ[R] M₂) (φ : Module.End R M₁) :
    (e.conj φ).charpoly = φ.charpoly

Proof state:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ ((LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ)).charpoly = ((LinearMap.toMatrix b b) φ).charpoly

Tactic:
congr 1

Result:
case e_M
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) = (LinearMap.toMatrix b b) φ

Proof state:
case e_M.a
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
i j : ChooseBasisIndex R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) i j = (LinearMap.toMatrix b b) φ i j

Tactic:
simp [Matrix.charmatrix, LinearMap.toMatrix, Matrix.diagonal, LinearEquiv.conj_apply]

Result:
no goals

Proof state:
case e_M
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) = (LinearMap.toMatrix b b) φ

Tactic:
ext i j : 1

Result:
case e_M.a
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
i j : ChooseBasisIndex R M₁
⊢ (LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) i j = (LinearMap.toMatrix b b) φ i j

Proof state:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ

Tactic:
rw [← LinearMap.charpoly_toMatrix φ b, ← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)]

Result:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ ((LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ)).charpoly = ((LinearMap.toMatrix b b) φ).charpoly

Proof state:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
⊢ LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ

Tactic:
let b := chooseBasis R M₁

Result:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : Nontrivial R
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module R M₁
inst✝⁵ : Module.Finite R M₁
inst✝⁴ : Module.Free R M₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Module.Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : Module.End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ