no goals
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ ↑(LieEquiv.symm (lieConj P h)) A = P⁻¹ ⬝ A ⬝ P
simp [LinearEquiv.symm_conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
  LinearMap.toMatrix'_toLin']