-- Module: Mathlib.RingTheory.Polynomial.Resultant.Basic
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
i j : Fin (m + (n + 1))
succ :
  ∀ (j : Fin m),
    Eq.{u_1 + 1} (α := R)
      (Fin.addCases (motive := fun (x : Fin (m + 1 + (n + 1))) ↦ R)
          (fun (j₁ : Fin (m + 1)) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (n + 1) then g.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (fun (j₁ : Fin (n + 1)) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (m + 1) then f.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)) (Fin.cast (n := m + (n + 1)) ⋯ (Fin.castAdd (n + 1) j))) :
        R)
      (Fin.addCases (motive := fun (x : Fin (m + (n + 1))) ↦ R)
          (fun (j₁ : Fin m) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (n + 1) then g.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (fun (j₁ : Fin (n + 1)) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (Fin.castAdd (n + 1) j) :
        R)
succ₁ :
  ∀ (j : Fin (n + 1)),
    Eq.{u_1 + 1} (α := R)
      (Fin.addCases (motive := fun (x : Fin (m + 1 + (n + 1))) ↦ R)
          (fun (j₁ : Fin (m + 1)) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (n + 1) then g.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (fun (j₁ : Fin (n + 1)) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (m + 1) then f.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)) (Fin.cast ⋯ (Fin.natAdd m j))) :
        R)
      (Fin.addCases (motive := fun (x : Fin (m + (n + 1))) ↦ R)
          (fun (j₁ : Fin m) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (n + 1) then g.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (fun (j₁ : Fin (n + 1)) ↦
            if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
          (Fin.natAdd m j) :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    (Fin.addCases (motive := fun (x : Fin (m + 1 + (n + 1))) ↦ R)
        (fun (j₁ : Fin (m + 1)) ↦
          if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (n + 1) then g.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
        (fun (j₁ : Fin (n + 1)) ↦
          if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (m + 1) then f.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
        (Fin.succAbove (Fin.castAdd (n + 1) (Fin.last m)) (Fin.cast ⋯ j)) :
      R)
    (Fin.addCases (motive := fun (x : Fin (m + (n + 1))) ↦ R)
        (fun (j₁ : Fin m) ↦
          if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + (n + 1) then g.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
        (fun (j₁ : Fin (n + 1)) ↦
          if (↑j₁ : ℕ) ≤ (↑i : ℕ) ∧ (↑i : ℕ) ≤ (↑j₁ : ℕ) + m then f.coeff ((↑i : ℕ) - (↑j₁ : ℕ)) else 0)
        j :
      R)

Tactic:
induction j using Fin.addCases with
      | left j =>
        have : ((Fin.last m).castAdd (n + 1)).succAbove ((j.castAdd (n + 1)).cast (by grind)) =
          j.castSucc.castAdd (n + 1) := by ext; simp [Fin.succAbove, Fin.lt_def]
        simp [this]
      | right j =>
        have : ((Fin.last m).castAdd (n + 1)).succAbove ((j.natAdd m).cast (by grind)) =
          j.natAdd _ := by ext; simp [Fin.succAbove, Fin.lt_def, add_right_comm]
        simp only [ite_and, this, Fin.addCases_right]
        split_ifs with h₁ h₂ h₃ h₃ <;> try lia
        exact coeff_eq_zero_of_natDegree_lt (by lia)

Premises used: Fin.addCases_right, Polynomial.coeff_eq_zero_of_natDegree_lt, ite_and