awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
rw : f ≠ 0
⊢ f.natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree

Tactic:
rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]

Premises used: Iff.mpr, Polynomial.natDegree_C_mul_X_pow, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
df : natDegree.{u_1} (R := R) 0 ≤ N
hf : #(support.{u_1} (R := R) 0) = n + 1 + 1
⊢ False

Tactic:
simp at hf
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N

Tactic:
(natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df

Premises used: Polynomial.leadingCoeff, LE.le.trans, Polynomial.natDegree, Polynomial.natDegree_C_mul_X_pow_le
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N

Tactic:
exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df

Premises used: Polynomial.leadingCoeff, LE.le.trans, Polynomial.natDegree, Polynomial.natDegree_C_mul_X_pow_le
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ motive f.eraseLead

Tactic:
hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)

Premises used: Polynomial.card_support_eraseLead', LE.le.trans, Polynomial.eraseLead_natDegree_le_aux
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ motive f.eraseLead

Tactic:
exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)

Premises used: Polynomial.card_support_eraseLead', LE.le.trans, Polynomial.eraseLead_natDegree_le_aux
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
C_mul_pow _ _ ?_ df
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
succ : f.leadingCoeff ≠ 0
⊢ motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
refine C_mul_pow _ _ ?_ df
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
succ : ¬n + 1 + 1 = 0
⊢ f.leadingCoeff ≠ 0

Tactic:
rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]

Premises used: Ne, Polynomial.card_support_eq_zero, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ ¬n + 1 + 1 = 0

Tactic:
Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ ¬n + 1 + 1 = 0

Tactic:
exact Nat.succ_ne_zero _

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
induction : ∀ (x : ℕ) (hf : #f.support = x), motive f
⊢ motive f

Tactic:
induction hf : #f.support generalizing f with
  | zero =>
    convert! zero
    simpa [support_eq_empty, card_eq_zero] using hf
  | succ c hc =>
    rw [← eraseLead_add_C_mul_X_pow f]
    cases c
    · convert! C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
      · convert! zero_add (C (leadingCoeff f) * X ^ f.natDegree)
        rw [← card_support_eq_zero, card_support_eraseLead' hf]
      · rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]
        exact zero_ne_one.symm
    refine add f.eraseLead _ ?_ ?_ ?_ ?_
    · refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
      · exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge
      · rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
        rintro rfl
        simp at hf
    · exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
    · exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)
    · refine C_mul_pow _ _ ?_ df
      rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]
      exact Nat.succ_ne_zero _

Premises used: Iff.mpr, Polynomial.C, HMul.hMul, Polynomial.eraseLead_add_C_mul_X_pow, zero_ne_one, Polynomial.leadingCoeff, Ne, Ne.symm, Polynomial.eraseLead, zero_add, Polynomial.natDegree_C_mul_X_pow, Polynomial.card_support_eq_zero, Nat.succ_ne_zero, HPow.hPow, Polynomial.leadingCoeff_ne_zero, LT.lt.trans_le, Finset.card_eq_zero, Polynomial.eraseLead_natDegree_lt, Polynomial.support_eq_empty, LE.le.trans, le_of_eq, Polynomial.natDegree, Polynomial.X, DFunLike.coe, Polynomial.leadingCoeff_eq_zero, Polynomial.support, Polynomial.natDegree_C_mul_X_pow_le, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
⊢ (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) 0

Tactic:
simp [fu0]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
refine_1 :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 →
      n ≤ p.natDegree →
        (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
refine_2 :
  ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ p.natDegree →
        (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) f →
          (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) g →
            (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) (f + g)
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree

Tactic:
refine induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree)
    p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le

Premises used: Polynomial.induction_with_natDegree_le, Eq.le, Polynomial.natDegree, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
n : ℕ
r : R
r0 : r ≠ 0
refine_1 :
  n ≤ p.natDegree →
    natDegree.{u_2} (R := S)
        ((φ : (a : R[X]) → S[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
      fu (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree
⊢ n ≤ p.natDegree →
    (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
n : ℕ
r : R
r0 : r ≠ 0
h : n ≤ p.natDegree
refine_1 :
  natDegree.{u_2} (R := S)
      ((φ : (a : R[X]) → S[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    fu n
refine_1₁ : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) r)) = fu n
refine_1₂ refine_1₃ : fu n = fu n
⊢ natDegree.{u_2} (R := S)
      ((φ : (a : R[X]) → S[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    fu (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree

Tactic:
rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.natDegree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
refine_2 :
  g.natDegree ≤ p.natDegree →
    (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) f →
      (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) g →
        (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) (f + g)
⊢ g.natDegree ≤ p.natDegree →
    (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) f →
      (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) g →
        (fun (p : R[X]) ↦ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree) (f + g)

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
refine_2 :
  (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
    fu g.natDegree
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) (f + g)) = fu (f + g).natDegree

Tactic:
rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]

Premises used: map_add, Polynomial.natDegree_add_eq_right_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
pos :
  ∀ (FG : k ≤ f.natDegree),
    (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X])
          ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
      fu g.natDegree
neg :
  ∀ (FG : f.natDegree < k),
    (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X])
          ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
      fu g.natDegree
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
    fu g.natDegree

Tactic:
by_cases! FG : k ≤ f.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
FG : k ≤ f.natDegree
pos : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) < natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g)
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
    fu g.natDegree

Tactic:
rw [natDegree_add_eq_right_of_natDegree_lt, gk]

Premises used: Polynomial.natDegree_add_eq_right_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
FG : k ≤ f.natDegree
pos : fu f.natDegree < fu g.natDegree
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) < natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g)

Tactic:
rw [fk, gk]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < fu g.natDegree

Tactic:
fc FG fg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < fu g.natDegree

Tactic:
exact fc FG fg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
FG : f.natDegree < k
neg :
  ∀ (fu0 : ∀ {n : ℕ}, n ≤ 0 → fu n = 0) (fc : ∀ {n m : ℕ}, 0 ≤ n → n < m → fu n < fu m)
    (φ_k : ∀ {f : R[X]}, f.natDegree < 0 → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X]))
    (FG : f.natDegree < 0),
    (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X])
          ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
      fu g.natDegree
neg₁ :
  ∀ (n : ℕ) (fu0 : ∀ {n_1 : ℕ}, n_1 ≤ n + 1 → fu n_1 = 0) (fc : ∀ {n_1 m : ℕ}, n + 1 ≤ n_1 → n_1 < m → fu n_1 < fu m)
    (φ_k : ∀ {f : R[X]}, f.natDegree < n + 1 → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X]))
    (FG : f.natDegree < n + 1),
    (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X])
          ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
      fu g.natDegree
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
    fu g.natDegree

Tactic:
cases k