-- Lean 4 proof step from Mathlib.Algebra.Lie.Basis (goal)
Goal:
ι : Type u_1
K : Type u_2
L : Type u_3
inst : Fintype ι
inst_1 : Field K
inst_2 : CharZero K
inst_3 : LieRing L
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
b : Basis ι K L
inst_6 : IsTriangularizable K (↥b.cartan) L
inst_7 : IsKilling K L
this :
  (reindex (Equiv.symm b.baseSupportEquiv) (Equiv.symm b.baseSupportEquiv) :
        (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
      (RootPairing.Base.cartanMatrix b.base) =
    b.A
⊢ Eq (α :=
    Matrix
      ↥(RootPairing.Base.support (M := Dual.{u_2, u_3} K ↥b.cartan) (N := ↥b.cartan) (P :=
            (rootSystem b.cartan :
              RootPairing (↥(root : Finset (Weight K (↥b.cartan) L))) K (Dual.{u_2, u_3} K ↥b.cartan) ↥b.cartan))
            (b.base : RootPairing.Base (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)) :
          Finset ↥(root : Finset (Weight K (↥b.cartan) L)))
      ↥(RootPairing.Base.support (M := Dual.{u_2, u_3} K ↥b.cartan) (N := ↥b.cartan) (P :=
            (rootSystem b.cartan :
              RootPairing (↥(root : Finset (Weight K (↥b.cartan) L))) K (Dual.{u_2, u_3} K ↥b.cartan) ↥b.cartan))
            (b.base : RootPairing.Base (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)) :
          Finset ↥(root : Finset (Weight K (↥b.cartan) L)))
      ℤ)
    (RootPairing.Base.cartanMatrix b.base :
      Matrix
        ↥(RootPairing.Base.support (M := Dual.{u_2, u_3} K ↥b.cartan) (N := ↥b.cartan) (P :=
              (rootSystem b.cartan :
                RootPairing (↥(root : Finset (Weight K (↥b.cartan) L))) K (Dual.{u_2, u_3} K ↥b.cartan) ↥b.cartan))
              (b.base : RootPairing.Base (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)) :
            Finset ↥(root : Finset (Weight K (↥b.cartan) L)))
        ↥(RootPairing.Base.support (M := Dual.{u_2, u_3} K ↥b.cartan) (N := ↥b.cartan) (P :=
              (rootSystem b.cartan :
                RootPairing (↥(root : Finset (Weight K (↥b.cartan) L))) K (Dual.{u_2, u_3} K ↥b.cartan) ↥b.cartan))
              (b.base : RootPairing.Base (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)) :
            Finset ↥(root : Finset (Weight K (↥b.cartan) L)))
        ℤ)
    ((reindex b.baseSupportEquiv b.baseSupportEquiv : (a : Matrix ι ι ℤ) → Matrix ↥b.base.support ↥b.base.support ℤ)
        b.A :
      Matrix
        ↥(RootPairing.Base.support (M := Dual.{u_2, u_3} K ↥b.cartan) (N := ↥b.cartan) (P :=
              (rootSystem b.cartan :
                RootPairing (↥(root : Finset (Weight K (↥b.cartan) L))) K (Dual.{u_2, u_3} K ↥b.cartan) ↥b.cartan))
              (b.base : RootPairing.Base (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)) :
            Finset ↥(root : Finset (Weight K (↥b.cartan) L)))
        ↥(RootPairing.Base.support (M := Dual.{u_2, u_3} K ↥b.cartan) (N := ↥b.cartan) (P :=
              (rootSystem b.cartan :
                RootPairing (↥(root : Finset (Weight K (↥b.cartan) L))) K (Dual.{u_2, u_3} K ↥b.cartan) ↥b.cartan))
              (b.base : RootPairing.Base (ι := ↥(root : Finset (Weight K (↥b.cartan) L))) (rootSystem b.cartan)) :
            Finset ↥(root : Finset (Weight K (↥b.cartan) L)))
        ℤ)
have rwa : (Equiv.symm (reindex b.baseSupportEquiv b.baseSupportEquiv) :
      (a : Matrix ↥b.base.support ↥b.base.support ℤ) → Matrix ι ι ℤ)
    (RootPairing.Base.cartanMatrix b.base) =
  b.A
Tactic: rwa [← (reindex b.baseSupportEquiv b.baseSupportEquiv).symm_apply_eq]