-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : (i : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R :=
  fun (i : ℕ) ↦
    (Matrix.of : (a : Fin (m + n) → Fin (m + n) → R) → Matrix (Fin (m + n)) (Fin (m + n)) R) fun (j₁ j₂ : Fin (m + n)) ↦
      if (↑j₂ : ℕ) < i then M₁ j₁ j₂ else M₂ j₁ j₂
j₁ j₂ : Fin (m + n)
IH : ∀ (hi : (↑j₂ : ℕ) ≤ m), (M (↑j₂ : ℕ)).det = r ^ (↑j₂ : ℕ) * M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
succ :
  ∀ (j₂ : Fin m)
    (IH :
      ∀ (hi : (↑(Fin.castAdd n j₂) : ℕ) ≤ m),
        (M (↑(Fin.castAdd n j₂) : ℕ)).det = r ^ (↑(Fin.castAdd n j₂) : ℕ) * M₂.det)
    (hi : (↑(Fin.castAdd n j₂) : ℕ) + 1 ≤ m),
    HMul.hMul (β := R) r
        (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
            (fun (j₁_1 : Fin m) ↦
              if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
            (fun (j₁_1 : Fin n) ↦
              if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
            (Fin.castAdd n j₂) :
          R) =
      Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
        (fun (j₁_1 : Fin m) ↦
          if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then r * g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
        (fun (j₁_1 : Fin n) ↦
          if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
        (Fin.castAdd n j₂)
⊢ HMul.hMul (β := R) r
      (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
          (fun (j₁_1 : Fin m) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (fun (j₁_1 : Fin n) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          j₂ :
        R) =
    Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
      (fun (j₁_1 : Fin m) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then r * g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (fun (j₁_1 : Fin n) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      j₂
have succ₁ : ∀ (i : Fin n)
  (IH : ∀ (hi : (↑(Fin.natAdd m i) : ℕ) ≤ m), (M (↑(Fin.natAdd m i) : ℕ)).det = r ^ (↑(Fin.natAdd m i) : ℕ) * M₂.det)
  (hi : (↑(Fin.natAdd m i) : ℕ) + 1 ≤ m),
  HMul.hMul (β := R) r
      (Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
          (fun (j₁_1 : Fin m) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (fun (j₁_1 : Fin n) ↦
            if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
          (Fin.natAdd m i) :
        R) =
    Fin.addCases (motive := fun (x : Fin (m + n)) ↦ R)
      (fun (j₁_1 : Fin m) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + n then r * g.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (fun (j₁_1 : Fin n) ↦
        if (↑j₁_1 : ℕ) ≤ (↑j₁ : ℕ) ∧ (↑j₁ : ℕ) ≤ (↑j₁_1 : ℕ) + m then f.coeff ((↑j₁ : ℕ) - (↑j₁_1 : ℕ)) else 0)
      (Fin.natAdd m i)
Tactic: induction j₂ using Fin.addCases with
        | left j₂ => simp
        | right i => simp at hi
Cleared hypotheses: j₂, IH, hi