case mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
⊢ IsPrime (map C P) → IsPrime P

case mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
⊢ IsPrime P → IsPrime (map C P)
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
⊢ IsPrime (map C P) ↔ IsPrime P
constructor
case mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
⊢ IsPrime P
case mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
⊢ IsPrime (map C P) → IsPrime P
intro H
case mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
⊢ IsPrime P
case mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
⊢ IsPrime P
have := @comap_isPrime R R[X] (R →+* R[X]) _ _ _ C (map C P) H
case h.e'_3
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
⊢ P = comap C (map C P)
case mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
⊢ IsPrime P
convert this using 1
case h.e'_3.h
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ x ∈ P ↔ x ∈ comap C (map C P)
case h.e'_3
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
⊢ P = comap C (map C P)
ext x
case h.e'_3.h
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ x ∈ P ↔ ∀ (n : ℕ), coeff (↑C x) n ∈ P
case h.e'_3.h
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ x ∈ P ↔ x ∈ comap C (map C P)
simp only [mem_comap, mem_map_C_iff]
case h.e'_3.h.mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ x ∈ P → ∀ (n : ℕ), coeff (↑C x) n ∈ P

case h.e'_3.h.mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ (∀ (n : ℕ), coeff (↑C x) n ∈ P) → x ∈ P
case h.e'_3.h
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ x ∈ P ↔ ∀ (n : ℕ), coeff (↑C x) n ∈ P
constructor
case h.e'_3.h.mp.zero
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
h : x ∈ P
⊢ coeff (↑C x) Nat.zero ∈ P

case h.e'_3.h.mp.succ
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
h : x ∈ P
n : ℕ
⊢ coeff (↑C x) (Nat.succ n) ∈ P
case h.e'_3.h.mp
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ x ∈ P → ∀ (n : ℕ), coeff (↑C x) n ∈ P
rintro h (- | n)
no goals
case h.e'_3.h.mp.zero
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
h : x ∈ P
⊢ coeff (↑C x) Nat.zero ∈ P
rwa [coeff_C_zero]
no goals
case h.e'_3.h.mp.succ
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
h : x ∈ P
n : ℕ
⊢ coeff (↑C x) (Nat.succ n) ∈ P
simp only [coeff_C_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]
case h.e'_3.h.mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
h : ∀ (n : ℕ), coeff (↑C x) n ∈ P
⊢ x ∈ P
case h.e'_3.h.mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
⊢ (∀ (n : ℕ), coeff (↑C x) n ∈ P) → x ∈ P
intro h
no goals
case h.e'_3.h.mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
H : IsPrime (map C P)
this : IsPrime (comap C (map C P))
x : R
h : ∀ (n : ℕ), coeff (↑C x) n ∈ P
⊢ x ∈ P
simpa only [coeff_C_zero] using h 0
case mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ IsPrime (map C P)
case mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
⊢ IsPrime P → IsPrime (map C P)
intro h
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ map C P ≠ ⊤

case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ∀ {x y : R[X]}, x * y ∈ map C P → x ∈ map C P ∨ y ∈ map C P
case mpr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ IsPrime (map C P)
constructor
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ∃ x, ¬coeff 1 x ∈ P
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ map C P ≠ ⊤
rw [Ne.def, eq_top_iff_one, mem_map_C_iff, not_forall]
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ¬coeff 1 0 ∈ P
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ∃ x, ¬coeff 1 x ∈ P
use 0
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ¬P = ⊤
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ¬coeff 1 0 ∈ P
rw [coeff_one_zero, ← eq_top_iff_one]
no goals
case mpr.ne_top'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ¬P = ⊤
exact h.1
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
⊢ f * g ∈ map C P → f ∈ map C P ∨ g ∈ map C P
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
⊢ ∀ {x y : R[X]}, x * y ∈ map C P → x ∈ map C P ∨ y ∈ map C P
intro f g
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
⊢ (∀ (n : ℕ), coeff (f * g) n ∈ P) → (∀ (n : ℕ), coeff f n ∈ P) ∨ ∀ (n : ℕ), coeff g n ∈ P
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
⊢ f * g ∈ map C P → f ∈ map C P ∨ g ∈ map C P
simp only [mem_map_C_iff]
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
⊢ ((∃ n, ¬coeff f n ∈ P) ∧ ∃ n, ¬coeff g n ∈ P) → ∃ n, ¬coeff (f * g) n ∈ P
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
⊢ (∀ (n : ℕ), coeff (f * g) n ∈ P) → (∀ (n : ℕ), coeff f n ∈ P) ∨ ∀ (n : ℕ), coeff g n ∈ P
contrapose!
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
⊢ ∃ n, ¬coeff (f * g) n ∈ P
case mpr.mem_or_mem'
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
⊢ ((∃ n, ¬coeff f n ∈ P) ∧ ∃ n, ¬coeff g n ∈ P) → ∃ n, ¬coeff (f * g) n ∈ P
rintro ⟨hf, hg⟩
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
⊢ ∃ n, ¬coeff (f * g) n ∈ P
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
⊢ ∃ n, ¬coeff (f * g) n ∈ P
let m := Nat.find hf
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∃ n, ¬coeff (f * g) n ∈ P
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
⊢ ∃ n, ¬coeff (f * g) n ∈ P
let n := Nat.find hg
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬coeff (f * g) (m + n) ∈ P
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∃ n, ¬coeff (f * g) n ∈ P
refine' ⟨m + n, _⟩
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬coeff f (m, n).fst * coeff g (m, n).snd ∈ P

R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x in Finset.erase (Nat.antidiagonal ((m, n).fst + (m, n).snd)) (m, n), coeff f x.fst * coeff g x.snd ∈ P
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬coeff (f * g) (m + n) ∈ P
rw [coeff_mul, ← Finset.insert_erase ((@Finset.Nat.mem_antidiagonal _ (m, n)).mpr rfl),
  Finset.sum_insert (Finset.not_mem_erase _ _), (P.add_mem_iff_left _).not]
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∀ (c : ℕ × ℕ),
    c ∈ Finset.erase (Nat.antidiagonal ((m, n).fst + (m, n).snd)) (m, n) → coeff f c.fst * coeff g c.snd ∈ P
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x in Finset.erase (Nat.antidiagonal ((m, n).fst + (m, n).snd)) (m, n), coeff f x.fst * coeff g x.snd ∈ P
apply P.sum_mem
case mk
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ∈ Finset.erase (Nat.antidiagonal ((m, n).fst + (m, n).snd)) (m, n)
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∀ (c : ℕ × ℕ),
    c ∈ Finset.erase (Nat.antidiagonal ((m, n).fst + (m, n).snd)) (m, n) → coeff f c.fst * coeff g c.snd ∈ P
rintro ⟨i, j⟩ hij
case mk
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).fst + (i, j).snd = (m, n).fst + (m, n).snd
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
case mk
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ∈ Finset.erase (Nat.antidiagonal ((m, n).fst + (m, n).snd)) (m, n)
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
rw [Finset.mem_erase, Finset.Nat.mem_antidiagonal] at hij
case mk
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
case mk
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).fst + (i, j).snd = (m, n).fst + (m, n).snd
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
simp only [Ne.def, Prod.mk.inj_iff, not_and_or] at hij
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬(coeff f (m, n).fst ∈ P ∨ coeff g (m, n).snd ∈ P)
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬coeff f (m, n).fst * coeff g (m, n).snd ∈ P
apply mt h.2
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬coeff f (m, n).fst ∈ P ∧ ¬coeff g (m, n).snd ∈ P
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬(coeff f (m, n).fst ∈ P ∨ coeff g (m, n).snd ∈ P)
rw [not_or]
no goals
case mpr.mem_or_mem'.intro
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ¬coeff f (m, n).fst ∈ P ∧ ¬coeff g (m, n).snd ∈ P
exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
⊢ m < i ∨ m = i → j < n
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
⊢ i < m ∨ j < n
rw [or_iff_not_imp_left, not_lt, le_iff_lt_or_eq]
case inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hmi : m < i
⊢ j < n

case inr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
j : ℕ
hij : (¬m = Nat.find hf ∨ ¬j = Nat.find hg) ∧ m + j = Nat.find hf + Nat.find hg
⊢ j < n
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
⊢ m < i ∨ m = i → j < n
rintro (hmi | rfl)
case inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hmi : m < i
⊢ ¬n ≤ j
case inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hmi : m < i
⊢ j < n
rw [← not_le]
case inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hmi : m < i
hnj : n ≤ j
⊢ False
case inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hmi : m < i
⊢ ¬n ≤ j
intro hnj
no goals
case inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hmi : m < i
hnj : n ≤ j
⊢ False
exact (add_lt_add_of_lt_of_le hmi hnj).ne hij.2.symm
no goals
case inr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
j : ℕ
hij : (¬m = Nat.find hf ∨ ¬j = Nat.find hg) ∧ m + j = Nat.find hf + Nat.find hg
⊢ j < n
simp only [eq_self_iff_true, not_true, false_or_iff, add_right_inj,
  not_and_self_iff] at hij
case mk.inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hi : i < m
⊢ coeff g (i, j).snd * coeff f (i, j).fst ∈ P
case mk.inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hi : i < m
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
rw [mul_comm]
case mk.inl.a
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hi : i < m
⊢ coeff f (i, j).fst ∈ P
case mk.inl
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hi : i < m
⊢ coeff g (i, j).snd * coeff f (i, j).fst ∈ P
apply P.mul_mem_left
no goals
case mk.inl.a
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hi : i < m
⊢ coeff f (i, j).fst ∈ P
exact Classical.not_not.1 (Nat.find_min hf hi)
case mk.inr.a
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hj : j < n
⊢ coeff g (i, j).snd ∈ P
case mk.inr
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hj : j < n
⊢ coeff f (i, j).fst * coeff g (i, j).snd ∈ P
apply P.mul_mem_left
no goals
case mk.inr.a
R : Type u
S : Type ?u.241035
inst✝ : CommRing R
P : Ideal R
h : IsPrime P
f g : R[X]
hf : ∃ n, ¬coeff f n ∈ P
hg : ∃ n, ¬coeff g n ∈ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = Nat.find hf ∨ ¬j = Nat.find hg) ∧ i + j = Nat.find hf + Nat.find hg
hj : j < n
⊢ coeff g (i, j).snd ∈ P
exact Classical.not_not.1 (Nat.find_min hg hj)