awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf_1 : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f g : R[X]
h : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) f
h_1 : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) g
hf : ∀ (n : ℕ), f.coeff n ∈ I
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ (f + g).coeff n ∈ I

Tactic:
simp [I.add_mem (hf n) (hg n)]

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
⊢ ∀ (x y : R[X])
    (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x)
    (hy : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) y),
    (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I

Tactic:
exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
⊢ ∀ (a x : R[X])
    (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x),
    (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Tactic:
fun f g _ hg n => ?_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f
mp :
  ∀ (f g : R[X]),
    Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) g →
      ∀ (hg : ∀ (n : ℕ), g.coeff n ∈ I) (n : ℕ), (f • g).coeff n ∈ I
⊢ ∀ (a x : R[X])
    (hx : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) x),
    (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Tactic:
refine fun f g _ hg n => ?_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f g : R[X]
h : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) g
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
mp : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2 ∈ I
⊢ (f • g).coeff n ∈ I

Tactic:
rw [smul_eq_mul, coeff_mul]

Premises used: Polynomial.coeff_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f g : R[X]
h : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) g
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2 ∈ I

Tactic:
I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Premises used: Set.Mem, Submodule.sum_mem, Prod.fst, Polynomial.coeff, Ideal.mul_mem_left, Prod.snd
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f_1 : R[X]
hf : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f_1
f g : R[X]
h : Membership.mem (γ := Submodule R[X] R[X]) (Submodule.span R[X] ((⇑C : (a : R) → R[X]) '' (↑I : Set R))) g
hg : ∀ (n : ℕ), g.coeff n ∈ I
n : ℕ
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2 ∈ I

Tactic:
exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
mpr :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I)
    (f.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I) f

Tactic:
rw [← sum_monomial_eq f]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I)
    (f.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)

Tactic:
(I.map C : Ideal R[X]).sum_mem fun n _ => ?_

Premises used: Polynomial.C, Set.Mem, Polynomial.sum, Submodule.sum_mem, Ideal.map
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
mpr :
  ∀ 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))
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C I)
    (f.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)

Tactic:
refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_

Premises used: Polynomial.C, Submodule.sum_mem, Ideal.map
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
h : n ∈ f.support
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))
⊢ 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))

Tactic:
simp only [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
h : n ∈ f.support
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]))
⊢ 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:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Basic
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]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (f.coeff n) : R[X]))

Tactic:
(I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Premises used: Polynomial.C, Ideal.mem_map_of_mem, Set.Mem, Ideal.map, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
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]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (f.coeff n) : R[X]))

Tactic:
exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Premises used: Polynomial.C, Ideal.mem_map_of_mem, Ideal.map, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : CommSemiring R
inst_1 : Semiring S
f : R →+* S
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
⊢ Eq (α := Ideal R[X]) (RingHom.ker (mapRingHom f)) (map (F := R →+* R[X]) C (RingHom.ker f))

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : CommSemiring R
inst_1 : Semiring S
f : R →+* S
x : R[X]
h :
  (∀ (n : ℕ), (Polynomial.map f x).coeff n = coeff 0 n) ↔
    ∀ (n : ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (x.coeff n)
⊢ Polynomial.map f x = 0 ↔ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (RingHom.ker f)) x

Tactic:
rw [mem_map_C_iff, Polynomial.ext_iff]

Premises used: Polynomial.ext_iff, Ideal.mem_map_C_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : CommSemiring R
inst_1 : Semiring S
f : R →+* S
x : R[X]
⊢ (∀ (n : ℕ), (Polynomial.map f x).coeff n = coeff 0 n) ↔
    ∀ (n : ℕ), Membership.mem (γ := Ideal R) (RingHom.ker f) (x.coeff n)

Tactic:
simp [RingHom.mem_ker]

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
simp :
  (∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) ↔
    ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x
⊢ x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x

Tactic:
simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
    mem_degreeLE]

Premises used: Submodule.mem_map, Ideal.leadingCoeffNth, Polynomial.lcoeff_apply, Submodule.mem_inf, Ideal.degreeLE, Polynomial.mem_degreeLE
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
mpr :
  (∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = x) →
    ∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x
⊢ (∃ (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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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

Tactic:
rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg

Premises used: lt_or_eq_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

Tactic:
⟨0, I.zero_mem, bot_le, ?_⟩

Premises used: Ideal.zero_mem, And.intro, Exists.intro, OfNat.ofNat, bot_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : Polynomial.leadingCoeff 0 = p.coeff n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n

Tactic:
refine ⟨0, I.zero_mem, bot_le, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 n = 0
⊢ Polynomial.leadingCoeff 0 = p.coeff n

Tactic:
rw [leadingCoeff_zero, eq_comm]

Premises used: Polynomial.leadingCoeff_zero, eq_comm
-- Module: Mathlib.RingTheory.Polynomial.Basic
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.coeff n = 0

Tactic:
coeff_eq_zero_of_degree_lt hpdeg

Premises used: Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.Basic
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.coeff n = 0

Tactic:
exact coeff_eq_zero_of_degree_lt hpdeg

Premises used: Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

Tactic:
⟨p, hpI, le_of_eq hpdeg, ?_⟩

Premises used: And.intro, Exists.intro, le_of_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
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.leadingCoeff = p.coeff n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.coeff n

Tactic:
refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
mp₄ mp₅ : p.coeff n = p.coeff n
⊢ p.leadingCoeff = p.coeff n

Tactic:
rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]

Premises used: Polynomial.leadingCoeff, Nat.cast_withBot, WithBot.unbotD_coe, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ (↑n : WithBot ℕ)
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

Tactic:
⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, Ideal.mul_mem_right, And.intro, Exists.intro, Polynomial.natDegree, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)
mpr₁ : (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.leadingCoeff
⊢ ∃ (y : R[X]), (y.degree ≤ (↑n : WithBot ℕ) ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = p.leadingCoeff

Tactic:
refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
apply : p.degree + (HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)
⊢ (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)

Tactic:
apply le_trans (degree_mul_le _ _) _

Premises used: Polynomial.degree_mul_le, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
apply : HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(n - p.natDegree) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ p.degree + (HPow.hPow (α := R[X]) X (n - p.natDegree)).degree ≤ (↑n : WithBot ℕ)

Tactic:
apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _

Premises used: add_le_add, Polynomial.degree_X_pow_le, Polynomial.degree_le_natDegree, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)
rw₁ rw₂ : LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(n - p.natDegree) : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
rw [← Nat.cast_add, this]

Premises used: Nat.cast_add
-- Module: Mathlib.RingTheory.Polynomial.Basic
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))
mpr₂ mpr₃ :
  (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n
⊢ (p * HPow.hPow (α := R[X]) X (n - p.natDegree)).coeff n = p.leadingCoeff

Tactic:
rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

Premises used: Polynomial.coeff_mul_X_pow, HSub.hSub, Polynomial.leadingCoeff, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
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])
rwa₂ : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rwa₃ rwa₄ rwa₅ rwa₆ : p ∈ I
⊢ Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : 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]

Premises used: Polynomial.leadingCoeff, Polynomial.eq_C_of_degree_le_zero, Polynomial.natDegree_le_of_degree_le, Nat.eq_zero_of_le_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ I.leadingCoeffNth m
simp :
  ∀ (hr : ∃ p ∈ I, p.degree ≤ (↑m : WithBot ℕ) ∧ p.leadingCoeff = r),
    ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = r
⊢ r ∈ I.leadingCoeffNth n

Tactic:
simp only [mem_leadingCoeffNth] at hr ⊢

Premises used: Ideal.mem_leadingCoeffNth
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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
⊢ ∃ p ∈ I, p.degree ≤ (↑n : WithBot ℕ) ∧ p.leadingCoeff = r

Tactic:
rcases hr with ⟨p, hpI, hpdeg, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

Tactic:
⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩

Premises used: Polynomial.leadingCoeff_mul_X_pow, HMul.hMul, HSub.hSub, HPow.hPow, Ideal.mul_mem_right, And.intro, Exists.intro, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)
refine : (p * HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)
⊢ ∃ p_1 ∈ I, p_1.degree ≤ (↑n : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff

Tactic:
refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)

Tactic:
le_trans (degree_mul_le _ _) ?_

Premises used: Polynomial.degree_mul_le, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)
refine : p.degree + (HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)
⊢ (p * HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)

Tactic:
refine le_trans (degree_mul_le _ _) ?_

Premises used: Polynomial.degree_mul_le, le_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)
grw : HAdd.hAdd (α := WithBot ℕ) (↑m : WithBot ℕ) (↑(n - m) : WithBot ℕ) ≤ (↑n : WithBot ℕ)
⊢ p.degree + (HPow.hPow (α := R[X]) X (n - m)).degree ≤ (↑n : WithBot ℕ)

Tactic:
grw [hpdeg, degree_X_pow_le]

Premises used: Polynomial.degree_X_pow_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 ℕ)
rw₁ rw₂ : LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ HAdd.hAdd (α := WithBot ℕ) (↑m : WithBot ℕ) (↑(n - m) : WithBot ℕ) ≤ (↑n : WithBot ℕ)

Tactic:
rw [← Nat.cast_add, add_tsub_cancel_of_le H]

Premises used: Nat.cast_add, add_tsub_cancel_of_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
rw : (∃ (i : ℕ), x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x
H : Directed (fun (x1 x2 : Submodule R R) ↦ x1 ≤ x2) fun (n : ℕ) ↦ I.leadingCoeffNth n
⊢ x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
rw [leadingCoeff, Submodule.mem_iSup_of_directed]

Premises used: Ideal.leadingCoeff, Submodule.mem_iSup_of_directed
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
simp : (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) ↔ ∃ p ∈ I, p.leadingCoeff = x
⊢ (∃ (i : ℕ), x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
simp only [mem_leadingCoeffNth]

Premises used: Ideal.mem_leadingCoeffNth
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
mpr : (∃ p ∈ I, p.leadingCoeff = x) → ∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x
⊢ (∃ (i : ℕ), ∃ p ∈ I, p.degree ≤ (↑i : WithBot ℕ) ∧ p.leadingCoeff = x) ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
i : ℕ
p : R[X]
hpI : p ∈ I
left : p.degree ≤ (↑i : WithBot ℕ)
⊢ ∃ p_1 ∈ I, p_1.leadingCoeff = p.leadingCoeff

Tactic:
⟨p, hpI, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
i : ℕ
p : R[X]
hpI : p ∈ I
left : p.degree ≤ (↑i : WithBot ℕ)
⊢ ∃ p_1 ∈ I, p_1.leadingCoeff = p.leadingCoeff

Tactic:
exact ⟨p, hpI, rfl⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ (i : ℕ), ∃ p_1 ∈ I, p_1.degree ≤ (↑i : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff

Tactic:
⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩

Premises used: Polynomial.degree_le_natDegree, And.intro, Exists.intro, Polynomial.natDegree, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ (i : ℕ), ∃ p_1 ∈ I, p_1.degree ≤ (↑i : WithBot ℕ) ∧ p_1.leadingCoeff = p.leadingCoeff

Tactic:
exact ⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩