-- 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₂
j₁ j₂ : Fin (m + n)
IH : ∀ (hi : (↑j₂ : ℕ) ≤ m), (M (↑j₂ : ℕ)).det = M₂.det
hi : (↑j₂ : ℕ) + 1 ≤ m
succ :
  ∀ (j₂ : Fin m) (IH : ∀ (hi : (↑(Fin.castAdd n j₂) : ℕ) ≤ m), (M (↑(Fin.castAdd n j₂) : ℕ)).det = M₂.det)
    (hi : (↑(Fin.castAdd n j₂) : ℕ) + 1 ≤ m),
    HSub.hSub (α := 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 : ℕ)) +
                  (HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])).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)
        (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₂) : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) :
            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₂)
succ₁ :
  ∀ (i : Fin n) (IH : ∀ (hi : (↑(Fin.natAdd m i) : ℕ) ≤ m), (M (↑(Fin.natAdd m i) : ℕ)).det = M₂.det)
    (hi : (↑(Fin.natAdd m i) : ℕ) + 1 ≤ m),
    HSub.hSub (α := 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 : ℕ)) +
                  (HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])).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)
        (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) : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) :
            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)
⊢ HSub.hSub (α := 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 : ℕ)) +
                (HMul.hMul (β := R[X]) f ((monomial k : (a : R) → R[X]) r : R[X])).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)
      (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₂ : ℕ) + (k + m), ⋯⟩ : Fin (m + n)) :
          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₂

Tactic:
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

Premises used: add_sub_assoc, Fin.addCases_left, sub_eq_zero, add_assoc, ite_add_zero, mul_assoc, Polynomial.C_mul_X_pow_eq_monomial, mul_ite, sub_eq_self, Polynomial.coeff_mul_C, MulZeroClass.mul_zero, Fin.addCases_right, Fin.val_castAdd, add_eq_left, Polynomial.coeff_eq_zero_of_natDegree_lt, mul_comm, tsub_add_eq_tsub_tsub, ite_and, Polynomial.coeff_mul_X_pow', Fin.val_natAdd, LE.le.trans_lt, if_neg