-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
r : R
m n k : ℕ
hk : k + m ≤ n
hf : f.natDegree ≤ m
hm : m ≠ 0
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R :=
  f.sylvester (g + HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])) 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₂
i : ℕ
hi : i ≤ m
zero : ∀ (hi : 0 ≤ m), (M 0).det = M₂.det
succ : ∀ (i : ℕ) (IH : ∀ (hi : i ≤ m), (M i).det = M₂.det) (hi : i + 1 ≤ m), (M (i + 1)).det = M₂.det
⊢ (M i).det = M₂.det

Tactic:
induction i with
    | zero => simp [M]; rfl
    | succ i IH =>
      rw [← IH (by lia), ← Matrix.det_updateCol_add_smul_self (i := ⟨i, by lia⟩)
        (j := ⟨i + k + m, by lia⟩) (c := -r) (M (i + 1)) (by simp; lia)]
      congr 1
      ext j₁ j₂
      simp only [Matrix.of_apply, lt_add_iff_pos_right, zero_lt_one, ↓reduceIte, add_assoc,
        add_lt_add_iff_left, Nat.lt_one_iff, Nat.add_eq_zero_iff, hm, and_false, smul_eq_mul,
        Matrix.updateCol_apply, Fin.ext_iff, M, M₂, neg_mul, ← sub_eq_add_neg]
      obtain rfl | h := eq_or_ne ↑j₂ i
      · simp only [↓reduceIte, sylvester, Set.mem_Icc, coeff_add, Fin.eta, Matrix.of_apply,
          lt_self_iff_false, M₁]
        induction j₂ using Fin.addCases with
        | left j₂ =>
          dsimp at hi
          have : Fin.mk (n := m + n) (↑j₂ + (k + m)) (by lia) = .natAdd m ⟨j₂ + k, by lia⟩ :=
            Fin.ext (by simp; lia)
          simp only [Fin.addCases_left, Fin.val_castAdd, this, Fin.addCases_right, mul_ite,
            mul_zero, ← C_mul_X_pow_eq_monomial, ← mul_assoc, coeff_mul_X_pow', ite_add_zero,
            coeff_mul_C, add_assoc, add_eq_left, ← ite_and, ← mul_comm r, tsub_add_eq_tsub_tsub,
            add_sub_assoc, sub_eq_zero]
          split_ifs with h₁ h₂ h₂ <;> try rfl
          · rw [coeff_eq_zero_of_natDegree_lt, mul_zero]
            exact hf.trans_lt (by lia)
          · lia
        | right i =>
          simp only [Fin.val_natAdd] at hi
          have : Fin.mk (n := m + n) (m + ↑i + (k + m)) (by lia) =
              Fin.natAdd m ⟨↑i + (k + m), by lia⟩ := Fin.ext (by simp; lia)
          simp only [Fin.addCases_right, Fin.val_natAdd, sub_eq_self, this]
          rw [if_neg, mul_zero]
          lia
      lia

Premises used: add_sub_assoc, Fin.addCases_left, lt_add_iff_pos_right, Fin.ext_iff, sub_eq_zero, add_assoc, Matrix.updateCol_apply, ite_add_zero, mul_assoc, sub_eq_add_neg, Polynomial.C_mul_X_pow_eq_monomial, mul_ite, sub_eq_self, Fin.eta, Polynomial.coeff_add, Matrix.of_apply, Polynomial.coeff_mul_C, MulZeroClass.mul_zero, Fin.addCases_right, zero_lt_one, Fin.val_castAdd, add_eq_left, Polynomial.sylvester, HAdd.hAdd, lt_self_iff_false, Nat.lt_one_iff, Polynomial.coeff_eq_zero_of_natDegree_lt, Matrix.det_updateCol_add_smul_self, mul_comm, Set.mem_Icc, eq_or_ne, reduceIte, neg_mul, and_false, tsub_add_eq_tsub_tsub, smul_eq_mul, ite_and, Polynomial.coeff_mul_X_pow', OfNat.ofNat, Fin.val_natAdd, LE.le.trans_lt, if_neg, Nat.add_eq_zero_iff, Neg.neg, rfl, add_lt_add_iff_left