awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 0
⊢ p.degree = 1
have h₃ : Eq (α := WithBot ℕ) 1 0
Tactic: rw [h₁] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
hgu : IsUnit g
⊢ p.degree = 1
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g).degree = 1
Tactic: rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
hgu : IsUnit g
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g).degree = 1
⊢ p.degree = 1
have rw₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree + g.degree = 1
Tactic: rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
hgu : IsUnit g
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g).degree = 1
rw₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree + g.degree = 1
⊢ p.degree = 1
have rw₂ : 1 + g.degree = 1
Tactic: rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
hgu : IsUnit g
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g).degree = 1
rw₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree + g.degree = 1
rw₂ : 1 + g.degree = 1
⊢ p.degree = 1
have rw₃ : HAdd.hAdd (α := WithBot ℕ) 1 0 = 1
Tactic: rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
hgu : IsUnit g
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g).degree = 1
rw₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree + g.degree = 1
rw₂ : 1 + g.degree = 1
rw₃ : HAdd.hAdd (α := WithBot ℕ) 1 0 = 1
⊢ p.degree = 1
have rw₄ : Eq (α := WithBot ℕ) 1 1
Tactic: rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
have inst : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
have inl : ∀ (hd : p.degree < 0),
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
Tactic: rcases hp.lt_or_gt with hd | hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
inl :
  ∀ (hd : p.degree < 0),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
have inr : ∀ (hd : 0 < p.degree),
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
Tactic: rcases hp.lt_or_gt with hd | hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : p.degree < 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
have inl : (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = leadingCoeff 0
Tactic: rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : p.degree < 0
inl : (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = leadingCoeff 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
have inl₁ : Eq.{u + 1} (α := R) (leadingCoeff 0) (leadingCoeff 0)
Tactic: rw [degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd, zero_divByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : 0 < p.degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff
have inr : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ p.degree
Tactic: refine leadingCoeff_divByMonic_of_monic (monic_X_sub_C a) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst_2 : Nontrivial R
hd : 0 < p.degree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ p.degree
have inr : 1 ≤ p.degree
Tactic: rwa [degree_X_sub_C, Nat.WithBot.one_le_iff_zero_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
⊢ p = q
have inl : ∀ (hpq : p ∣ 0) (h₁ : natDegree.{u} (R := R) 0 ≤ p.natDegree) (h₂ : p.leadingCoeff = leadingCoeff 0), p = 0
Tactic: rcases eq_or_ne q 0 with rfl | hq
Cleared hypotheses: q, hpq, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
inl : ∀ (hpq : p ∣ 0) (h₁ : natDegree.{u} (R := R) 0 ≤ p.natDegree) (h₂ : p.leadingCoeff = leadingCoeff 0), p = 0
⊢ p = q
have inr : ∀ (hq : q ≠ 0), p = q
Tactic: rcases eq_or_ne q 0 with rfl | hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p = q
have h₃ : p.natDegree = q.natDegree
Tactic: replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
hpq : p ∣ q
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
h₁ : p.natDegree = q.natDegree
⊢ p = q
have inr : ∀ (u : R[X]) (h₂ : p.leadingCoeff = (p * u).leadingCoeff) (hq : p * u ≠ 0) (h₁ : p.natDegree = (p * u).natDegree),
  p = p * u
Tactic: obtain ⟨u, rfl⟩ := hpq
Cleared hypotheses: q, hpq, h₂, hq, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p * u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u
have hq₁ : p ≠ 0 ∧ u ≠ 0
Tactic: rw [mul_ne_zero_iff] at hq
Cleared hypotheses: hq, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u
have h₃ : u.natDegree = 0
Tactic: rw [natDegree_mul hq.1 hq.2, left_eq_add] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
have h₃ : u.coeff 0 = 1
Tactic: rw [eq_C_of_natDegree_eq_zero h₁, leadingCoeff_mul, leadingCoeff_C,
    eq_comm, mul_eq_left₀ (leadingCoeff_ne_zero.mpr hq.1)] at h₂
Cleared hypotheses: h₂, hq, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
have inr : p = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (u.coeff 0) : R[X])
Tactic: rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
inr : p = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (u.coeff 0) : R[X])
⊢ p = p * u
have inr₁ : p = p * (C : (a : R) → R[X]) 1
Tactic: rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
inr : p = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (u.coeff 0) : R[X])
inr₁ : p = p * (C : (a : R) → R[X]) 1
⊢ p = p * u
have inr₂ : p = p * 1
Tactic: rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p u : R[X]
h₂ : u.coeff 0 = 1
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
inr : p = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (u.coeff 0) : R[X])
inr₁ : p = p * (C : (a : R) → R[X]) 1
inr₂ : p = p * 1
⊢ p = p * u
have inr₃ : p = p
Tactic: rw [eq_C_of_natDegree_eq_zero h₁, h₂, map_one, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
K : Type u_1
inst : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
⊢ IsUnit q.leadingCoeff
have rwa : ∀ (hq : q.leadingCoeff ≠ 0) (h₁ : q.natDegree ≤ p.natDegree), IsUnit q.leadingCoeff
Tactic: rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq
Cleared hypotheses: hq, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
K : Type u_1
inst : Field K
p q : K[X]
hpq : p ∣ q
hq : q ≠ 0
h₁ : q.natDegree ≤ p.natDegree
rwa : ∀ (hq : q.leadingCoeff ≠ 0) (h₁ : q.natDegree ≤ p.natDegree), IsUnit q.leadingCoeff
⊢ IsUnit q.leadingCoeff
have rwa₁ : ∀ (hq : IsUnit q.leadingCoeff) (h₁ : q.natDegree ≤ p.natDegree), IsUnit q.leadingCoeff
Tactic: rwa [← leadingCoeff_ne_zero, ← isUnit_iff_ne_zero] at hq
Cleared hypotheses: hq, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) p
have rw : q = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
Tactic: rw [mul_comm, ← eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
rw : q = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X])
⊢ q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) p
have rw₁ : q = q
Tactic: rw [mul_comm, ← eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    f
have rw : HAdd.hAdd (β := R[X]) f.eraseLead ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f
Tactic: rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
rw : HAdd.hAdd (β := R[X]) f.eraseLead ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f
⊢ f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    f
have rw₁ : f = f
Tactic: rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
f : R[X]
⊢ f - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    f.eraseLead
have rw : HSub.hSub (β := R[X]) f ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f.eraseLead
Tactic: rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
f : R[X]
rw : HSub.hSub (β := R[X]) f ((monomial f.natDegree : (a : R) → R[X]) f.leadingCoeff : R[X]) = f.eraseLead
⊢ f - HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    f.eraseLead
have rw₁ : f.eraseLead = f.eraseLead
Tactic: rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead ≠ 0
have rw : ¬#(f.support.erase f.natDegree) = 0
Tactic: rw [Ne, ← card_support_eq_zero, eraseLead_support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.eraseLead.support
⊢ a < f.natDegree
have h₁ : a ≠ f.natDegree ∧ a ∈ f.support
Tactic: rw [eraseLead_support, mem_erase] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support < #f.support
have rw : #(f.support.erase f.natDegree) < #f.support
Tactic: rw [eraseLead_support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
⊢ #f.eraseLead.support + 1 = #f.support
have set : let c := #f.support;
∀ (hc : c = #f.support), #f.eraseLead.support + 1 = c
Tactic: set c := #f.support with hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
⊢ #f.eraseLead.support + 1 = c
have cases : ∀ (h₁ : c = 0), #f.eraseLead.support + 1 = 0
Tactic: cases h₁ : c
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
cases : ∀ (h₁ : c = 0), #f.eraseLead.support + 1 = 0
⊢ #f.eraseLead.support + 1 = c
have cases₁ : ∀ (n : ℕ) (h₁ : c = n + 1), #f.eraseLead.support + 1 = n + 1
Tactic: cases h₁ : c
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0
have by_contra : ∀ (this : ¬#f.eraseLead.support + 1 = 0), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
⊢ #f.eraseLead.support + 1 = n + 1
have rw : n + 1 - 1 + 1 = n + 1
Tactic: rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
⊢ #f.eraseLead.support + 1 = n + 1
have case : #(f.support.erase f.natDegree) + 1 = n + 1
Tactic: case succ =>
    rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
    rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
case : #(f.support.erase f.natDegree) + 1 = n + 1
⊢ #f.eraseLead.support + 1 = n + 1
have case₁ : #f.support - 1 + 1 = n + 1
Tactic: case succ =>
    rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
    rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n : ℕ
h₁ : c = n + 1
case : #(f.support.erase f.natDegree) + 1 = n + 1
case₁ : #f.support - 1 + 1 = n + 1
case₂ : c - 1 + 1 = n + 1
⊢ #f.eraseLead.support + 1 = n + 1
have case₃ : n + 1 - 1 + 1 = n + 1
Tactic: case succ =>
    rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
    rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ #f.eraseLead.support = #f.support - 1
have pos : ∀ (hf : f = 0), #f.eraseLead.support = #f.support - 1
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (hf : f = 0), #f.eraseLead.support = #f.support - 1
⊢ #f.eraseLead.support = #f.support - 1
have neg : ∀ (hf : ¬f = 0), #f.eraseLead.support = #f.support - 1
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
⊢ #f.eraseLead.support = #f.support - 1
have pos : #(support.{u_1} (R := R) (eraseLead 0)) = #(support.{u_1} (R := R) 0) - 1
Tactic: rw [hf, eraseLead_zero, support_zero, card_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
pos : #(support.{u_1} (R := R) (eraseLead 0)) = #(support.{u_1} (R := R) 0) - 1
⊢ #f.eraseLead.support = #f.support - 1
have pos₁ : #(support.{u_1} (R := R) 0) = #(support.{u_1} (R := R) 0) - 1
Tactic: rw [hf, eraseLead_zero, support_zero, card_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
pos : #(support.{u_1} (R := R) (eraseLead 0)) = #(support.{u_1} (R := R) 0) - 1
pos₁ : #(support.{u_1} (R := R) 0) = #(support.{u_1} (R := R) 0) - 1
⊢ #f.eraseLead.support = #f.support - 1
have pos₂ : card (α := ℕ) ∅ = card (α := ℕ) ∅ - 1
Tactic: rw [hf, eraseLead_zero, support_zero, card_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f = 0
pos : #(support.{u_1} (R := R) (eraseLead 0)) = #(support.{u_1} (R := R) 0) - 1
pos₁ : #(support.{u_1} (R := R) 0) = #(support.{u_1} (R := R) 0) - 1
pos₂ : card (α := ℕ) ∅ = card (α := ℕ) ∅ - 1
⊢ #f.eraseLead.support = #f.support - 1
have pos₃ : 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [hf, eraseLead_zero, support_zero, card_empty]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
⊢ #f.eraseLead.support = #f.support - 1
have neg : #f.eraseLead.support = #f.eraseLead.support + 1 - 1
Tactic: rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : ¬f = 0
neg : #f.eraseLead.support = #f.eraseLead.support + 1 - 1
⊢ #f.eraseLead.support = #f.support - 1
have neg₁ : #f.eraseLead.support = #f.eraseLead.support
Tactic: rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.eraseLead.support = c
have rw : #f.support - 1 = c
Tactic: rw [card_support_eraseLead, fc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
rw : #f.support - 1 = c
⊢ #f.eraseLead.support = c
have rw₁ : c + 1 - 1 = c
Tactic: rw [card_support_eraseLead, fc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
rw : #f.support - 1 = c
rw₁ : c + 1 - 1 = c
⊢ #f.eraseLead.support = c
have rw₂ : c = c
Tactic: rw [card_support_eraseLead, fc, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ #f.support ≤ 1
have by_cases : ∀ (hpz : f = 0), #f.support ≤ 1
Tactic: by_cases hpz : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
by_cases : ∀ (hpz : f = 0), #f.support ≤ 1
⊢ #f.support ≤ 1
have by_cases₁ : ∀ (hpz : ¬f = 0), #f.support ≤ 1
Tactic: by_cases hpz : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have pos : ∀ (hr : r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
pos : ∀ (hr : r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have neg : ∀ (hr : ¬r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : r = 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have pos : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) 0)) 0
Tactic: subst r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have neg : Eq.{u_1 + 1} (α := R[X])
  (erase (natDegree.{u_1} (R := R) ((monomial i : (a : R) → R[X]) r)) ((monomial i : (a : R) → R[X]) r)) 0
Tactic: rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]