-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst : CommRing R
inst_1 : CommRing S
M : Matrix m m S
inst_2 : DecidableEq m
inst_3 : DecidableEq n
k : m
inst_4 : Fintype m
inst_5 : Fintype n
f : S →+* Matrix n n R
ih :
  ∀ (M : Matrix.{u_5, u_5, u_2} { a : m // (a = k) = False } { a : m // (a = k) = False } S),
    Eq.{u_1 + 1} (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (M.map (⇑f : (a : S) → Matrix n n R))))
rw :
  det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det) *
        HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) -
      det (n := m × n)
          ((Matrix.comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
            (M.map (⇑f : (a : S) → Matrix n n R))) *
        HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) =
    0
rw₁ :
  det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det) *
        HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) -
      HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k)))
        (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
          ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
              (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
                Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
            (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R)))) =
    0
⊢ HSub.hSub (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
        (det (n := m × n)
          ((Matrix.comp m m n n R : (a : Matrix m m (Matrix n n R)) → Matrix (m × n) (m × n) R)
            (M.map (⇑f : (a : S) → Matrix n n R)))) *
      HPow.hPow (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k))) (Fintype.card m - 1) =
    0
have rw₂ : det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det) *
      (HPow.hPow (α := Matrix n n R) ((f : (a : S) → Matrix n n R) (M k k) : Matrix n n R) (Fintype.card m - 1)).det -
    HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k)))
      (det (n := Prod.{u_5, u_4} { a : m // (a = k) = False } n)
        ((Matrix.comp { a : m // (a = k) = False } { a : m // (a = k) = False } n n R :
            (a : Matrix { a : m // (a = k) = False } { a : m // (a = k) = False } (Matrix n n R)) →
              Matrix ({ a : m // (a = k) = False } × n) ({ a : m // (a = k) = False } × n) R)
          (Matrix.map ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False) (⇑f : (a : S) → Matrix n n R)))) =
  0
Tactic: rw [sub_mul, comp_det_mul_pow, ← det_pow, ← map_pow, ← det_mul, ← map_mul,
    det_mul_corner_pow, map_mul, det_mul, ih, sub_self]