-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
a :
  ∀ (i j : m) (n_1 : ℕ),
    (HSub.hSub (α := Matrix (m ⊕ n) (m ⊕ n) R[X]) (β := Matrix (m ⊕ n) (m ⊕ n) R[X])
            ((scalar (m ⊕ n) : (a : R[X]) → Matrix (m ⊕ n) (m ⊕ n) R[X]) X : Matrix (m ⊕ n) (m ⊕ n) R[X])
            ((RingHom.mapMatrix C : (a : Matrix (m ⊕ n) (m ⊕ n) R) → Matrix (m ⊕ n) (m ⊕ n) R[X])
                (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) :
              Matrix (m ⊕ n) (m ⊕ n) R[X])
            (Sum.inl i) (Sum.inl j)).coeff
        n_1 =
      (fromBlocks
            (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
              ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
              ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M₁₁ : Matrix.{u_3, u_3, u_1} m m R[X]))
            (-M₁₂.map (⇑C : (a : R) → R[X])) (-M₂₁.map (⇑C : (a : R) → R[X]))
            (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
              ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
              ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M₂₂ : Matrix.{u_4, u_4, u_1} n n R[X]))
            (Sum.inl i) (Sum.inl j)).coeff
        n_1
⊢ HSub.hSub (α := Matrix (m ⊕ n) (m ⊕ n) R[X]) (β := Matrix (m ⊕ n) (m ⊕ n) R[X])
      ((scalar (m ⊕ n) : (a : R[X]) → Matrix (m ⊕ n) (m ⊕ n) R[X]) X : Matrix (m ⊕ n) (m ⊕ n) R[X])
      ((RingHom.mapMatrix C : (a : Matrix (m ⊕ n) (m ⊕ n) R) → Matrix (m ⊕ n) (m ⊕ n) R[X])
          (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) :
        Matrix (m ⊕ n) (m ⊕ n) R[X]) =
    fromBlocks
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M₁₁ : Matrix.{u_3, u_3, u_1} m m R[X]))
      (-M₁₂.map (⇑C : (a : R) → R[X])) (-M₂₁.map (⇑C : (a : R) → R[X]))
      (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
        ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M₂₂ : Matrix.{u_4, u_4, u_1} n n R[X]))
have a₁ : ∀ (i : m) (j : n) (n_1 : ℕ),
  (HSub.hSub (α := Matrix (m ⊕ n) (m ⊕ n) R[X]) (β := Matrix (m ⊕ n) (m ⊕ n) R[X])
          ((scalar (m ⊕ n) : (a : R[X]) → Matrix (m ⊕ n) (m ⊕ n) R[X]) X : Matrix (m ⊕ n) (m ⊕ n) R[X])
          ((RingHom.mapMatrix C : (a : Matrix (m ⊕ n) (m ⊕ n) R) → Matrix (m ⊕ n) (m ⊕ n) R[X])
              (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂) :
            Matrix (m ⊕ n) (m ⊕ n) R[X])
          (Sum.inl i) (Sum.inr j)).coeff
      n_1 =
    (fromBlocks
          (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
            ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
            ((RingHom.mapMatrix C : (a : Matrix m m R) → Matrix m m R[X]) M₁₁ : Matrix.{u_3, u_3, u_1} m m R[X]))
          (-M₁₂.map (⇑C : (a : R) → R[X])) (-M₂₁.map (⇑C : (a : R) → R[X]))
          (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
            ((RingHom.mapMatrix C : (a : Matrix n n R) → Matrix n n R[X]) M₂₂ : Matrix.{u_4, u_4, u_1} n n R[X]))
          (Sum.inl i) (Sum.inr j)).coeff
      n_1
Tactic: ext (i | i) (j | j) : 2