awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
h : n ∈ f.support
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C I)
    ((fun (n : ℕ) (a : R) ↦ ((monomial n : (a : R) → R[X]) a : R[X])) n (f.coeff n))
have mpr : Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C I)
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: simp only [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
h : n ∈ f.support
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C I)
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have mpr : Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C I)
  (HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (f.coeff n) : R[X]))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommSemiring R
inst_1 : Semiring S
f : R →+* S
⊢ Eq (α := Ideal R[X]) (RingHom.ker (mapRingHom f)) (map (F := R →+* R[X]) C (RingHom.ker f))
have h : ∀ (x : R[X]),
  Membership.mem (γ := Ideal R[X]) (RingHom.ker (mapRingHom f)) x ↔
    Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (RingHom.ker f)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
S : Type u_1
inst : CommSemiring R
inst_1 : Semiring S
f : R →+* S
x : R[X]
⊢ Polynomial.map f x = 0 ↔ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (RingHom.ker f)) x
have h : (∀ (n : ℕ), (Polynomial.map f x).coeff n = coeff 0 n) ↔
  ∀ (n : ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (x.coeff n)
Tactic: rw [mem_map_C_iff, Polynomial.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
have simp : (∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔
  ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
Tactic: simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
    mem_degreeLE]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔
    ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
have mp : (∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) →
  ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
mp :
  (∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) →
    ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
⊢ (∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔
    ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
have mpr : (∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x) →
  ∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
have mp : ∀ (hpdeg : p.degree < (↑n : WithBot ℕ)), ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
Tactic: rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
mp : ∀ (hpdeg : p.degree < (↑n : WithBot ℕ)), ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
have mp₁ : ∀ (hpdeg : p.degree = (↑n : WithBot ℕ)), ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
Tactic: rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < (↑n : WithBot ℕ)
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
have mp : Polynomial.leadingCoeff 0 = p.coeff n
Tactic: refine ⟨0, I.zero_mem, bot_le, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < (↑n : WithBot ℕ)
⊢ Polynomial.leadingCoeff 0 = p.coeff n
have mp : p.coeff n = 0
Tactic: rw [leadingCoeff_zero, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = (↑n : WithBot ℕ)
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n
have mp : p.leadingCoeff = p.coeff n
Tactic: refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = (↑n : WithBot ℕ)
⊢ p.leadingCoeff = p.coeff n
have mp : p.coeff p.natDegree = p.coeff n
Tactic: rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = (↑n : WithBot ℕ)
mp : p.coeff p.natDegree = p.coeff n
⊢ p.leadingCoeff = p.coeff n
have mp₁ : p.coeff (WithBot.unbotD 0 p.degree) = p.coeff n
Tactic: rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = (↑n : WithBot ℕ)
mp : p.coeff p.natDegree = p.coeff n
mp₁ : p.coeff (WithBot.unbotD 0 p.degree) = p.coeff n
⊢ p.leadingCoeff = p.coeff n
have mp₂ : p.coeff (WithBot.unbotD 0 (↑n : WithBot ℕ)) = p.coeff n
Tactic: rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = (↑n : WithBot ℕ)
mp : p.coeff p.natDegree = p.coeff n
mp₁ : p.coeff (WithBot.unbotD 0 p.degree) = p.coeff n
mp₂ : p.coeff (WithBot.unbotD 0 (↑n : WithBot ℕ)) = p.coeff n
⊢ p.leadingCoeff = p.coeff n
have mp₃ : p.coeff (WithBot.unbotD 0 (↑n : WithBot ℕ)) = p.coeff n
Tactic: rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg_1 : p.degree ≤ (↑n : WithBot ℕ)
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = (↑n : WithBot ℕ)
mp : p.coeff p.natDegree = p.coeff n
mp₁ : p.coeff (WithBot.unbotD 0 p.degree) = p.coeff n
mp₂ : p.coeff (WithBot.unbotD 0 (↑n : WithBot ℕ)) = p.coeff n
mp₃ : p.coeff (WithBot.unbotD 0 (↑n : WithBot ℕ)) = p.coeff n
⊢ p.leadingCoeff = p.coeff n
have mp₄ : p.coeff n = p.coeff n
Tactic: rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
⊢ ∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff
have this : p.natDegree + (n - p.natDegree) = n
Tactic: have : natDegree p + (n - natDegree p) = n :=
      add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
⊢ ∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff
have mpr : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)
Tactic: refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
mpr : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)
⊢ ∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff
have mpr₁ : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.leadingCoeff
Tactic: refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)
have apply : p.degree + (HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)
Tactic: apply le_trans (degree_mul_le _ _) _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
⊢ p.degree + (HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)
have apply : HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(n - p.natDegree) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
Tactic: apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
⊢ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(n - p.natDegree) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have rw : LE.le (α := WithBot ℕ) (↑(p.natDegree + (n - p.natDegree)) : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [← Nat.cast_add, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
rw : LE.le (α := WithBot ℕ) (↑(p.natDegree + (n - p.natDegree)) : WithBot ℕ) (↑n : WithBot ℕ)
⊢ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(n - p.natDegree) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have rw₁ : LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [← Nat.cast_add, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
⊢ (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.leadingCoeff
have mpr : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.coeff p.natDegree
Tactic: rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
mpr : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.coeff p.natDegree
⊢ (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.leadingCoeff
have mpr₁ : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n =
  (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff (p.natDegree + (n - p.natDegree))
Tactic: rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
this : p.natDegree + (n - p.natDegree) = n
mpr : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.coeff p.natDegree
mpr₁ :
  (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n =
    (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff (p.natDegree + (n - p.natDegree))
⊢ (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.leadingCoeff
have mpr₂ : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n
Tactic: rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
h : ∃ p ∈ I, p.degree ≤ (↑0 : WithBot ℕ) ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑0 : WithBot ℕ)
hpx : p.leadingCoeff = x
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
have rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
Tactic: rwa [← hpx, Polynomial.leadingCoeff,
        Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
h : ∃ p ∈ I, p.degree ≤ (↑0 : WithBot ℕ) ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑0 : WithBot ℕ)
hpx : p.leadingCoeff = x
rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
have rwa₁ : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
Tactic: rwa [← hpx, Polynomial.leadingCoeff,
        Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
h : ∃ p ∈ I, p.degree ≤ (↑0 : WithBot ℕ) ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑0 : WithBot ℕ)
hpx : p.leadingCoeff = x
rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
rwa₁ : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
have rwa₂ : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rwa [← hpx, Polynomial.leadingCoeff,
        Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ I.leadingCoeffNth m
⊢ r ∈ I.leadingCoeffNth n
have simp : ∀ (hr : ∃ p ∈ I, p.degree ≤ (↑m : WithBot ℕ) ∧ p.leadingCoeff = r),
  ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = r
Tactic: simp only [mem_leadingCoeffNth] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : ∃ p ∈ I, p.degree ≤ (↑m : WithBot ℕ) ∧ p.leadingCoeff = r
⊢ ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = r
have rcases : ∀ (p : R[X]) (hpI : p ∈ I) (hpdeg : p.degree ≤ (↑m : WithBot ℕ)),
  ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff
Tactic: rcases hr with ⟨p, hpI, hpdeg, rfl⟩
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑m : WithBot ℕ)
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff
have refine : (p * HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)
Tactic: refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑m : WithBot ℕ)
⊢ (p * HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)
have refine : p.degree + (HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)
Tactic: refine le_trans (degree_mul_le _ _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑m : WithBot ℕ)
⊢ p.degree + (HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)
have grw : HAdd.hAdd (α := WithBot ℕ) (↑m : WithBot ℕ) (↑(n - m) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
Tactic: grw [hpdeg, degree_X_pow_le]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑m : WithBot ℕ)
⊢ HAdd.hAdd (α := WithBot ℕ) (↑m : WithBot ℕ) (↑(n - m) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have rw : LE.le (α := WithBot ℕ) (↑(m + (n - m)) : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [← Nat.cast_add, add_tsub_cancel_of_le H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑m : WithBot ℕ)
rw : LE.le (α := WithBot ℕ) (↑(m + (n - m)) : WithBot ℕ) (↑n : WithBot ℕ)
⊢ HAdd.hAdd (α := WithBot ℕ) (↑m : WithBot ℕ) (↑(n - m) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
have rw₁ : LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [← Nat.cast_add, add_tsub_cancel_of_le H]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
⊢ x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x
have rw : (∃ (i : ℕ), x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x
Tactic: rw [leadingCoeff, Submodule.mem_iSup_of_directed]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
rw : (∃ (i : ℕ), x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x
⊢ x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x
have H : Directed (fun (x1 x2 : Submodule R R) ↦ x1 ≤ x2) fun (n : ℕ) ↦ I.leadingCoeffNth n
Tactic: rw [leadingCoeff, Submodule.mem_iSup_of_directed]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ (i : ℕ), x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x
have simp : (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) ↔ ∃ p ∈ I, p.leadingCoeff = x
Tactic: simp only [mem_leadingCoeffNth]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) ↔ ∃ p ∈ I, p.leadingCoeff = x
have mp : (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) → ∃ p ∈ I, p.leadingCoeff = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
mp : (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) → ∃ p ∈ I, p.leadingCoeff = x
⊢ (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) ↔ ∃ p ∈ I, p.leadingCoeff = x
have mpr : (∃ p ∈ I, p.leadingCoeff = x) → ∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
x : R
hx : x ∈ I.leadingCoeff
⊢ x ∈ J.leadingCoeff
have rcases : ∀ (p : R[X]) (hpI : p ∈ I) (hx : p.leadingCoeff ∈ I.leadingCoeff), p.leadingCoeff ∈ J.leadingCoeff
Tactic: rcases (I.mem_leadingCoeff x).1 hx with ⟨p, hpI, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
⊢ leadingCoeff (map (F := R →+* R[X]) C p) = p
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x ↔ x ∈ p
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
x : R
⊢ Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x ↔ x ∈ p
have h : Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x → x ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
x : R
h : Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x → x ∈ p
⊢ Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x ↔ x ∈ p
have h₁ : x ∈ p → Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
x : R
hx : Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x
⊢ x ∈ p
have h : ∀ (f : R[X]) (hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C p) f)
  (hx : Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) f.leadingCoeff), f.leadingCoeff ∈ p
Tactic: rcases ((map C p).mem_leadingCoeff x).1 hx with ⟨f, hf, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
I J : Ideal R[X]
⊢ I.leadingCoeff * J.leadingCoeff ≤ (I * J).leadingCoeff
have refine : ∀ r ∈ I.leadingCoeff, ∀ s ∈ J.leadingCoeff, r * s ∈ (I * J).leadingCoeff
Tactic: refine (mul_le).2 ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
hb : b ∈ J.leadingCoeff
⊢ a * b ∈ (I * J).leadingCoeff
have rcases : ∀ (p : R[X]) (hpI : p ∈ I) (hp : p.leadingCoeff = a), a * b ∈ (I * J).leadingCoeff
Tactic: rcases (I.mem_leadingCoeff a).1 ha with ⟨p, hpI, hp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
b : R
hb : b ∈ J.leadingCoeff
p : R[X]
hpI : p ∈ I
hp : p.leadingCoeff = a
⊢ a * b ∈ (I * J).leadingCoeff
have rcases : ∀ (q : R[X]) (hqJ : q ∈ J) (hq : q.leadingCoeff = b), a * b ∈ (I * J).leadingCoeff
Tactic: rcases (J.mem_leadingCoeff b).1 hb with ⟨q, hqJ, hq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
⊢ ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
have refine : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff →
      ∏ i ∈ insert a s, (f i).leadingCoeff ≤ ((insert a s).prod f).leadingCoeff
Tactic: refine Finset.induction_on s (by simp) ?_