awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
⊢ IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))

Tactic:
have := comap_isPrime C (map C P)
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
⊢ IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))

Tactic:
this
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
h : P = comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)
⊢ P.IsPrime

Tactic:
convert! this using 1
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
h : ∀ (x : R), x ∈ P ↔ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)) x
⊢ P = comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
h : x ∈ P ↔ ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
⊢ x ∈ P ↔ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)) x

Tactic:
simp only [mem_comap, mem_map_C_iff]

Premises used: Ideal.mem_map_C_iff, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
h : x ∈ P → ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
h₁ : (∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P) → x ∈ P
⊢ x ∈ P ↔ ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
h h₁ h₂ h₃ h₄ : x ∈ P
⊢ coeff ((C : (a : R) → R[X]) x) 0 ∈ P

Tactic:
rwa [coeff_C_zero]

Premises used: Polynomial.coeff_C_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
h : x ∈ P
n : ℕ
⊢ coeff ((C : (a : R) → R[X]) x) (n + 1) ∈ P

Tactic:
simp only [coeff_C_of_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]

Premises used: Nat.succ_ne_zero, Submodule.zero_mem, Polynomial.coeff_C_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
h : ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
⊢ x ∈ P

Tactic:
simpa only [coeff_C_zero] using h 0

Premises used: Polynomial.coeff_C_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
mpr : Ne (α := Ideal R[X]) (map (F := R →+* R[X]) C P) ⊤
mpr₁ :
  ∀ {x y : R[X]},
    Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) (x * y) →
      Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) x ∨
        Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) y
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
mpr : ∃ (x : ℕ), coeff 1 x ∉ P
⊢ Ne (α := Ideal R[X]) (map (F := R →+* R[X]) C P) ⊤

Tactic:
rw [Ne, eq_top_iff_one, mem_map_C_iff, not_forall]

Premises used: Ne, Ideal.eq_top_iff_one, Ideal.mem_map_C_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
h₁ : coeff 1 0 ∉ P
⊢ ∃ (x : ℕ), coeff 1 x ∉ P

Tactic:
use 0
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
h₁ : ¬P = ⊤
⊢ coeff 1 0 ∉ P

Tactic:
rw [coeff_one_zero, ← eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one, Polynomial.coeff_one_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤

Tactic:
h.1

Premises used: Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤

Tactic:
exact h.1

Premises used: Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
mpr : (∀ (n : ℕ), (f * g).coeff n ∈ P) → (∀ (n : ℕ), f.coeff n ∈ P) ∨ ∀ (n : ℕ), g.coeff n ∈ P
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) (f * g) →
    Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) f ∨
      Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) g

Tactic:
simp only [mem_map_C_iff]

Premises used: Ideal.mem_map_C_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
mpr : ((∃ (n : ℕ), f.coeff n ∉ P) ∧ ∃ (n : ℕ), g.coeff n ∉ P) → ∃ (n : ℕ), (f * g).coeff n ∉ P
⊢ (∀ (n : ℕ), (f * g).coeff n ∈ P) → (∀ (n : ℕ), f.coeff n ∈ P) ∨ ∀ (n : ℕ), g.coeff n ∈ P

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P

Tactic:
⟨m + n, ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
mpr : (f * g).coeff (m + n) ∉ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P

Tactic:
refine ⟨m + n, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
mpr : f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
rw : ∑ x ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P
⊢ (f * g).coeff (m + n) ∉ P

Tactic:
rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]

Premises used: Iff.mpr, Polynomial.coeff_mul, Iff.not, Finset.HasAntidiagonal.mem_antidiagonal, Ideal.add_mem_iff_left, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
mpr : ¬(f.coeff (m, n).1 ∈ P ∨ g.coeff (m, n).2 ∈ P)
⊢ f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P

Tactic:
apply mt h.2

Premises used: mt, Ideal.IsPrime.mem_or_mem'
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
mpr : f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P
⊢ ¬(f.coeff (m, n).1 ∈ P ∨ g.coeff (m, n).2 ∈ P)

Tactic:
rw [not_or]

Premises used: not_or
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P

Tactic:
⟨Nat.find_spec hf, Nat.find_spec hg⟩

Premises used: And.intro, Nat.find_spec
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P

Tactic:
exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
apply : ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
⊢ ∑ x ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P

Tactic:
apply P.sum_mem

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (i, j) ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n)
⊢ (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2

Tactic:
rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij

Premises used: Finset.mem_erase, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
⊢ (¬i = m ∨ ¬j = n) ∧ i + j = m + n

Tactic:
simp only [Ne, Prod.mk_inj, not_and_or] at hij

Premises used: Prod.mk_inj, Ne, not_and_or
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
⊢ i < m ∨ j < n

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
inl : ∀ (hi : i < m), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
inr : ∀ (hj : j < n), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
obtain hi | hj : i < m ∨ j < n := by
          lia
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
inl : g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
inl : f.coeff (i, j).1 ∈ P
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P

Tactic:
apply P.mul_mem_left

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 ∈ P

Tactic:
Classical.not_not.1 (Nat.find_min hf hi)

Premises used: Classical.not_not, Nat.find_min, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 ∈ P

Tactic:
exact Classical.not_not.1 (Nat.find_min hf hi)

Premises used: Classical.not_not, Nat.find_min, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hj : j < n
inr : g.coeff (i, j).2 ∈ P
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
apply P.mul_mem_left

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hj : j < n
⊢ g.coeff (i, j).2 ∈ P

Tactic:
Classical.not_not.1 (Nat.find_min hg hj)

Premises used: Classical.not_not, Nat.find_min, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hj : j < n
⊢ g.coeff (i, j).2 ∈ P

Tactic:
exact Classical.not_not.1 (Nat.find_min hg hj)

Premises used: Classical.not_not, Nat.find_min, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
S : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)

Tactic:
(isPrime_map_C_iff_isPrime P).mpr ‹_›

Premises used: Iff.mpr, Ideal.isPrime_map_C_iff_isPrime
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R[X]
n : ℕ
⊢ (I.degreeLE (↑n : WithBot ℕ)).FG

Tactic:
letI := Classical.decEq R
  isNoetherian_submodule_left.1
    (isNoetherian_of_fg_of_noetherian _ ⟨_, degreeLE_eq_span_X_pow.symm⟩) _

Premises used: Set.Mem, Polynomial.degreeLE, Nat.cast, Finset.range, Ideal.degreeLE, Ideal.ofPolynomial, HPow.hPow, HAdd.hAdd, isNoetherian_of_fg_of_noetherian, Exists.intro, Iff.mp, isNoetherian_submodule_left, OfNat.ofNat, Eq.symm, Polynomial.X, Polynomial.degreeLE_eq_span_X_pow, Finset.image
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
⊢ map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I) = I

Tactic:
le_antisymm map_comap_le (fun f hfI ↦ ?_)

Premises used: le_antisymm, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
refine :
  ∀ (f : R[X]) (hfI : f ∈ I),
    Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
⊢ map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I) = I

Tactic:
refine le_antisymm map_comap_le (fun f hfI ↦ ?_)

Premises used: le_antisymm, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
f : R[X]
hfI : f ∈ I
h :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
          Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f)
    (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = n),
    Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f

Tactic:
induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ _ ih

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) f.leadingCoeff

Tactic:
simpa [hI] using (I.mem_leadingCoeff f.leadingCoeff).2 ⟨f, hfI, 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 : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
have h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I) :=
    (map C (comap C I)).mul_mem_right (X ^ f.natDegree) <| mem_map_of_mem C <| by
      simpa [hI] using (I.mem_leadingCoeff f.leadingCoeff).2 ⟨f, hfI, rfl⟩
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
h :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
h₁ :
  ∀ (hlt : f.eraseLead.natDegree < f.natDegree),
    Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
h₂ :
  ∀ (hzero : f.eraseLead = 0),
    Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f

Tactic:
rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with hlt | hzero

Premises used: Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
h :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
hlt : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead ∈ I

Tactic:
simpa using I.sub_mem hfI (map_comap_le h)

Premises used: Ideal.sub_mem, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
h :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
hlt : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead ∈ I

Tactic:
have he : f.eraseLead ∈ I := by simpa using I.sub_mem hfI (map_comap_le h)
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
h :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f.eraseLead.natDegree < n

Tactic:
simpa [hn] using hlt
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
h :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f

Tactic:
simpa using (map C (comap C I)).add_mem (ih _ (by simpa [hn] using hlt) _ he rfl) h

Premises used: Polynomial.C, Ideal.add_mem, Ideal.map, Ideal.comap, rfl