-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
zero :
  ∀ {f : R[X]},
    #f.support = 0 →
      ∃ (k : Fin 0 → ℕ) (x : Fin 0 → R) (_ : StrictMono k) (_ : ∀ (i : Fin 0), x i ≠ 0),
        f = ∑ i : Fin 0, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ {f : R[X]},
        #f.support = n →
          ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
            f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))
    {f : R[X]},
    #f.support = n + 1 →
      ∃ (k : Fin (n + 1) → ℕ) (x : Fin (n + 1) → R) (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0),
        f = ∑ i : Fin (n + 1), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
⊢ #f.support = n →
    ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
      f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))

Tactic:
induction n generalizing f with
  | zero => exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
  | succ n hn =>
    intro h
    obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
    have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
    refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
    · intro i j hij
      have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_setOf_eq]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
      obtain ⟨i, rfl⟩ := hi
      rw [Fin.strictMono_castSucc.injective.extend_apply]
      by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
      · obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
      · rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finsetSum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim
    · intro i
      by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
      · obtain ⟨i, rfl⟩ := hi
        rw [Fin.strictMono_castSucc.injective.extend_apply]
        exact hx i
      · rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero
    · rw [Fin.sum_univ_castSucc]
      simp only [Fin.strictMono_castSucc.injective.extend_apply]
      rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
      all_goals exact H

Premises used: Fin.sum_univ_castSucc, Polynomial.eraseLead_add_C_mul_X_pow, Fin.castSucc_lt_castSucc_iff, Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.lt_natDegree_of_mem_eraseLead_support, Function.Injective.extend_apply, Finset.sum_eq_single, MulZeroClass.mul_zero, StrictMono.injective, Polynomial.card_support_eq_zero, Polynomial.coeff_X_pow_self, Nat.succ_ne_zero, Fin.strictMono_castSucc, Function.extend_apply', mul_one, Polynomial.leadingCoeff_eq_zero, rfl