-- Lean 4 proof step from Mathlib.Algebra.Lie.Classical (goal)
Goal:
l : Type u_4
R : Type u₂
inst : DecidableEq l
inst_1 : CommRing R
inst_2 : Fintype l
a :
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inl PUnit.unit))
a₁ :
  ∀ (j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inl (Sum.inr j₃))
a₂ :
  ∀ (val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inl PUnit.unit)) (Sum.inr val)
a₃ :
  ∀ (i₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inl PUnit.unit))
a₄ :
  ∀ (i₃ j₃ : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inl (Sum.inr j₃))
a₅ :
  ∀ (i₃ val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inl (Sum.inr i₃)) (Sum.inr val) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inl (Sum.inr i₃)) (Sum.inr val)
a₆ :
  ∀ (val : l),
    indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val) (Sum.inl (Sum.inl PUnit.unit)) =
      (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
          (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
        (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val) (Sum.inl (Sum.inl PUnit.unit))
⊢ Eq (α := Matrix.{u_4, u_4, u₂} ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R) (indefiniteDiagonal (Unit ⊕ l) l R)
    ((reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)))
have a₇ : ∀ (val j₃ : l),
  indefiniteDiagonal (Unit ⊕ l) l R (Sum.inr val) (Sum.inl (Sum.inr j₃)) =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm :
        (a : Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R) → Matrix ((Unit ⊕ l) ⊕ l) ((Unit ⊕ l) ⊕ l) R)
      (fromBlocks 1 0 0 (indefiniteDiagonal l l R)) (Sum.inr val) (Sum.inl (Sum.inr j₃))
Tactic: ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩