-- Module: Mathlib.RingTheory.Norm.Transitivity
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
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
rw₃ :
  HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) M.det))
        (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
rw₄ :
  (HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : S) → Matrix n n R) M.det : Matrix n n R)
          ((f : (a : S) → Matrix n n R) (M k k ^ (Fintype.card m - 1)) : Matrix n n R)).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
rw₅ :
  det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M.det * 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
rw₆ :
  det.{u_1, u_4} (n := n)
        ((f : (a : S) → Matrix n n R)
          (M k k *
            det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False))) -
      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
rw₇ :
  (HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : S) → Matrix n n R) (M k k) : Matrix n n R)
          ((f : (a : S) → Matrix n n R)
              (det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)) :
            Matrix n n R)).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
rw₈ :
  HMul.hMul (α := R) (det.{u_1, u_4} (n := n) ((f : (a : S) → Matrix n n R) (M k k)))
        (det.{u_1, u_4} (n := n)
          ((f : (a : S) → Matrix n n R)
            (det (n := { a : m // (a = k) = False }) ((M * auxMat M k).toSquareBlock (fun (x : m) ↦ x = k) False)))) -
      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
rw₉ :
  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)))) -
      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
rw₁₀ rw₁₁ : Eq.{u_1 + 1} (α := R) 0 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

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]

Premises used: sub_self, Algebra.Norm.Transitivity.comp_det_mul_pow, map_pow, sub_mul, Matrix.det_mul, map_mul, Matrix.det_pow, Algebra.Norm.Transitivity.det_mul_corner_pow