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
⊢ ↑(lieConj P h) A = P ⬝ A ⬝ P⁻¹
simp [LinearEquiv.conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
  LinearMap.toMatrix'_toLin']