awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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 +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have succ : f.eraseLead.natDegree <
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
Tactic: refine add f.eraseLead _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have succ₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤ N
Tactic: refine add f.eraseLead _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
succ₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have succ₂ : motive f.eraseLead
Tactic: refine add f.eraseLead _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
succ₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N
succ₂ : motive f.eraseLead
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have succ₃ : motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
Tactic: refine add f.eraseLead _ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ f.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
have succ : 2 ≤ #f.support
Tactic: refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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 : 2 ≤ #f.support
⊢ f.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
have succ₁ : f.natDegree =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
Tactic: refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ f.natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
have rw : f ≠ 0
Tactic: rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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))
have succ : f.leadingCoeff ≠ 0
Tactic: refine C_mul_pow _ _ ?_ df
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ f.leadingCoeff ≠ 0
have succ : ¬n + 1 + 1 = 0
Tactic: rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ motive f
have induction : ∀ (x : ℕ) (hf : #f.support = x), 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 _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree
have 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))
Tactic: refine induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree)
    p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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))
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) p) = fu p.natDegree
have 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)
Tactic: refine induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree)
    p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ 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
have 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
Tactic: rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ 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
have refine_1₁ : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) r)) = fu n
Tactic: rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ 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
have refine_1₂ : fu n = fu n
Tactic: rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) (f + g)) = fu (f + g).natDegree
have 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
Tactic: rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have 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
Tactic: by_cases! FG : k ≤ f.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have 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
Tactic: by_cases! FG : k ≤ f.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have pos : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) < natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g)
Tactic: rw [natDegree_add_eq_right_of_natDegree_lt, gk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) < natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g)
have pos : fu f.natDegree < fu g.natDegree
Tactic: rw [fk, gk]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have 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
Tactic: cases k
Cleared hypotheses: k, fu0, fc, φ_k, FG