awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ (z : ℕ),
    (fun (x1 x2 : Submodule R R) ↦ x1 ≤ x2) ((fun (n : ℕ) ↦ I.leadingCoeffNth n) i)
        ((fun (n : ℕ) ↦ I.leadingCoeffNth n) z) ∧
      (fun (x1 x2 : Submodule R R) ↦ x1 ≤ x2) ((fun (n : ℕ) ↦ I.leadingCoeffNth n) j)
        ((fun (n : ℕ) ↦ I.leadingCoeffNth n) z)

Tactic:
⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
      I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩

Premises used: Nat.le_add_right, Nat.le_add_left, HAdd.hAdd, And.intro, Exists.intro, Ideal.leadingCoeffNth_mono
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
x : R
i j : ℕ
⊢ ∃ (z : ℕ),
    (fun (x1 x2 : Submodule R R) ↦ x1 ≤ x2) ((fun (n : ℕ) ↦ I.leadingCoeffNth n) i)
        ((fun (n : ℕ) ↦ I.leadingCoeffNth n) z) ∧
      (fun (x1 x2 : Submodule R R) ↦ x1 ≤ x2) ((fun (n : ℕ) ↦ I.leadingCoeffNth n) j)
        ((fun (n : ℕ) ↦ I.leadingCoeffNth n) z)

Tactic:
exact
    ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
      I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
x : R
hx : x ∈ I.leadingCoeff
rcases : ∀ (p : R[X]) (hpI : p ∈ I) (hx : p.leadingCoeff ∈ I.leadingCoeff), p.leadingCoeff ∈ J.leadingCoeff
⊢ x ∈ J.leadingCoeff

Tactic:
rcases (I.mem_leadingCoeff x).1 hx with ⟨p, hpI, rfl⟩

Premises used: Ideal.mem_leadingCoeff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
p : R[X]
hpI : p ∈ I
hx : p.leadingCoeff ∈ I.leadingCoeff
⊢ p.leadingCoeff ∈ J.leadingCoeff

Tactic:
(J.mem_leadingCoeff p.leadingCoeff).2 ⟨p, hIJ hpI, rfl⟩

Premises used: Iff.mpr, Set.Mem, Polynomial.leadingCoeff, Ideal.mem_leadingCoeff, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
p : R[X]
hpI : p ∈ I
hx : p.leadingCoeff ∈ I.leadingCoeff
⊢ p.leadingCoeff ∈ J.leadingCoeff

Tactic:
exact (J.mem_leadingCoeff p.leadingCoeff).2 ⟨p, hIJ hpI, rfl⟩

Premises used: Iff.mpr, Polynomial.leadingCoeff, Ideal.mem_leadingCoeff, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
h : ∀ (x : R), Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x ↔ x ∈ p
⊢ leadingCoeff (map (F := R →+* R[X]) C p) = p

Tactic:
ext x
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
h₁ : x ∈ p → Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x
⊢ Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x ↔ x ∈ p

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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
⊢ x ∈ p

Tactic:
rcases ((map C p).mem_leadingCoeff x).1 hx with ⟨f, hf, rfl⟩

Premises used: Polynomial.C, Ideal.map, Ideal.mem_leadingCoeff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
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:
p.mem_map_C_iff.1 hf f.natDegree

Premises used: Set.Mem, Polynomial.leadingCoeff, Ideal.mem_map_C_iff, Iff.mp, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
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:
exact p.mem_map_C_iff.1 hf f.natDegree

Premises used: Ideal.mem_map_C_iff, Iff.mp, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
x : R
hx : x ∈ p
⊢ Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x

Tactic:
((map C p).mem_leadingCoeff x).2 ⟨C x, mem_map_of_mem C hx, leadingCoeff_C x⟩

Premises used: Iff.mpr, Polynomial.C, Ideal.mem_map_of_mem, Ideal.map, Ideal.mem_leadingCoeff, And.intro, Exists.intro, Polynomial.leadingCoeff_C, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
p : Ideal R
x : R
hx : x ∈ p
⊢ Membership.mem (γ := Ideal R) (leadingCoeff (map (F := R →+* R[X]) C p)) x

Tactic:
exact ((map C p).mem_leadingCoeff x).2 ⟨C x, mem_map_of_mem C hx, leadingCoeff_C x⟩

Premises used: Iff.mpr, Polynomial.C, Ideal.mem_map_of_mem, Ideal.map, Ideal.mem_leadingCoeff, And.intro, Exists.intro, Polynomial.leadingCoeff_C, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq.{u + 1} (α := Ideal R) (leadingCoeff ⊤) ⊤

Tactic:
simp [← map_top C]

Premises used: Polynomial.C, Ideal.map_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
I J : Ideal R[X]
⊢ I.leadingCoeff * J.leadingCoeff ≤ (I * J).leadingCoeff

Tactic:
(mul_le).2 ?_

Premises used: Iff.mpr, Set.Mem, Ideal.mul_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
I J : Ideal R[X]
refine : ∀ r ∈ I.leadingCoeff, ∀ s ∈ J.leadingCoeff, r * s ∈ (I * J).leadingCoeff
⊢ I.leadingCoeff * J.leadingCoeff ≤ (I * J).leadingCoeff

Tactic:
refine (mul_le).2 ?_

Premises used: Iff.mpr, Ideal.mul_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
rcases : ∀ (p : R[X]) (hpI : p ∈ I) (hp : p.leadingCoeff = a), a * b ∈ (I * J).leadingCoeff
⊢ a * b ∈ (I * J).leadingCoeff

Tactic:
rcases (I.mem_leadingCoeff a).1 ha with ⟨p, hpI, hp⟩

Premises used: Ideal.mem_leadingCoeff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
rcases : ∀ (q : R[X]) (hqJ : q ∈ J) (hq : q.leadingCoeff = b), a * b ∈ (I * J).leadingCoeff
⊢ a * b ∈ (I * J).leadingCoeff

Tactic:
rcases (J.mem_leadingCoeff b).1 hb with ⟨q, hqJ, hq⟩

Premises used: Ideal.mem_leadingCoeff, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
q : R[X]
hqJ : q ∈ J
hq : q.leadingCoeff = b
⊢ (p * q).leadingCoeff = a * b

Tactic:
simp [hp, hq]
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
q : R[X]
hqJ : q ∈ J
hq : q.leadingCoeff = b
⊢ a * b ∈ (I * J).leadingCoeff

Tactic:
exact ((I * J).mem_leadingCoeff (a * b)).2 ⟨p * q, mul_mem_mul hpI hqJ, by simp [hp, hq]⟩

Premises used: Iff.mpr, HMul.hMul, Ideal.mem_leadingCoeff, Ideal.mul_mem_mul, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
⊢ ∏ i ∈ ∅, (f i).leadingCoeff ≤ (Finset.prod ∅ f).leadingCoeff

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
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
⊢ ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff

Tactic:
refine Finset.induction_on s (by simp) ?_
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_2
s_1 : Finset ι
f : ι → Ideal R[X]
i : ι
s : Finset ι
hi : i ∉ s
hs : ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
⊢ ∏ i ∈ insert i s, (f i).leadingCoeff ≤ ((insert i s).prod f).leadingCoeff

Tactic:
simpa [hi] using (mul_mono_right hs).trans (leadingCoeff_mul_le (f i) (s.prod f))

Premises used: Ideal.leadingCoeff_mul_le, Finset.prod, LE.le.trans, Ideal.mul_mono_right
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
refine refine₁ :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (hs : ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff),
    ∏ i ∈ insert i s, (f i).leadingCoeff ≤ ((insert i s).prod f).leadingCoeff
⊢ ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff

Tactic:
classical
  refine Finset.induction_on s (by simp) ?_
  intro i s hi hs
  simpa [hi] using (mul_mono_right hs).trans (leadingCoeff_mul_le (f i) (s.prod f))
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R[X]
inst_1 : NoZeroDivisors R
n : ℕ
⊢ I.leadingCoeff ^ n ≤ (I ^ n).leadingCoeff

Tactic:
simpa using leadingCoeff_finset_prod_le (Finset.range n) fun _ ↦ I

Premises used: Ideal.leadingCoeff_finset_prod_le, Finset.range
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
empty : Membership.mem (γ := Ideal R) ⊤ (if k = 0 then 1 else 0)
⊢ (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)

Tactic:
rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]

Premises used: Polynomial.coeff_one, Finset.prod_empty, Ideal.one_eq_top, pow_zero, Finset.sum_empty, zero_tsub
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ Membership.mem (γ := Ideal R) ⊤ (if k = 0 then 1 else 0)

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ Membership.mem (γ := Ideal R) ⊤ (if k = 0 then 1 else 0)

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
insert :
  ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, (f a).coeff x.1 * coeff (∏ x ∈ s, f x) x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
⊢ ((Insert.insert a s).prod f).coeff k ∈ I ^ ((Insert.insert a s).sum n - k)

Tactic:
rw [sum_insert ha, prod_insert ha, coeff_mul]

Premises used: Finset.prod_insert, Polynomial.coeff_mul, Finset.sum_insert
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
insert :
  ∀ c ∈ @antidiagonal _ Nat.instAddMonoid _ k, (f a).coeff c.1 * coeff (∏ x ∈ s, f x) c.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, (f a).coeff x.1 * coeff (∏ x ∈ s, f x) x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ k
⊢ i + j = k

Tactic:
mem_antidiagonal.mp e

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ k
insert :
  ∀ (e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)),
    (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
obtain rfl : i + j = k := mem_antidiagonal.mp e

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
insert : (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))

Tactic:
apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub

Premises used: Ideal.pow_le_pow_right, add_tsub_add_le_tsub_add_tsub
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
insert : (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
⊢ (f a).coeff (i, j).1 ∈ I ^ (n a - i)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
⊢ coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (∑ x ∈ s, n x - j)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)

Tactic:
exact Ideal.mul_mem_mul (by grind) (by grind)

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
    (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k))
    (h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
    ((Insert.insert a s).prod f).coeff k ∈ I ^ ((Insert.insert a s).sum n - k)
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Tactic:
induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)

Premises used: Polynomial.coeff_one, Finset.prod_empty, Ideal.one_eq_top, pow_add, Polynomial.coeff_mul, Insert.insert, Ideal.mul_mem_mul, pow_zero, Ideal.pow_le_pow_right, add_tsub_add_le_tsub_add_tsub, Finset.sum_empty, Submodule.mem_top, sum_mem, rfl, zero_tsub
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
    (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k))
    (h : ∀ i ∈ Insert.insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
    ((Insert.insert a s).prod f).coeff k ∈ I ^ ((Insert.insert a s).sum n - k)
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Tactic:
classical
    induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)

Premises used: Polynomial.coeff_one, Finset.prod_empty, Ideal.one_eq_top, pow_add, Polynomial.coeff_mul, Insert.insert, Ideal.mul_mem_mul, pow_zero, Ideal.pow_le_pow_right, add_tsub_add_le_tsub_add_tsub, Finset.sum_empty, Submodule.mem_top, sum_mem, rfl, zero_tsub
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
obtain : ∀ (p : R[X]) (hp : X * p = 1), False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero

Premises used: Polynomial.X_ne_zero, IsField.mul_inv_cancel
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := right_ne_zero_of_mul_eq_one hp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ p.degree < (p * X).degree

Tactic:
have := degree_lt_degree_mul_X hp0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ p = 0

Tactic:
rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this

Premises used: Polynomial.degree, Nat.WithBot.lt_zero_iff, congr_arg, Polynomial.degree_one, Polynomial.X_mul, Polynomial.degree_eq_bot
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False

Tactic:
hp0 this
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p = 0
⊢ False

Tactic:
exact hp0 this
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
⊢ x = 0

Tactic:
Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)

Premises used: Iff.mpr, Classical.by_contradiction, Ideal.eq_top_iff_one, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
refine : ∀ (hx0 : ¬x = 0), 1 ∈ I
⊢ x = 0

Tactic:
refine Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)

Premises used: Iff.mpr, Classical.by_contradiction, Ideal.eq_top_iff_one, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
obtain : ∀ (y : R) (hy : x * y = 1), 1 ∈ I
⊢ 1 ∈ I

Tactic:
obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0

Premises used: IsField.mul_inv_cancel
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X]) ∈ I

Tactic:
I.mul_mem_left (C y) hx

Premises used: Polynomial.C, Ideal.mul_mem_left, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
h : 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])
⊢ 1 ∈ I

Tactic:
convert! I.mul_mem_left (C y) hx

Premises used: Polynomial.C, Ideal.mul_mem_left, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (y * x) : R[X])
h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (x * y) : R[X])
h₂ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
h₃ h₄ : Eq.{u + 1} (α := R[X]) 1 1
⊢ 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])

Tactic:
rw [← C.map_mul, hR.mul_comm y x, hy, map_one]

Premises used: Polynomial.C, IsField.mul_comm, map_one, RingHom.map_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
mp : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P) → P.IsPrime
mpr : P.IsPrime → IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P) ↔ P.IsPrime

Tactic:
constructor