-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem isPrime_map_C_iff_isPrime (P : Ideal R) :
    IsPrime (map (C : R →+* R[X]) P : Ideal R[X]) ↔ IsPrime P

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ P.IsPrime → (map C P).IsPrime

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ (map C P).IsPrime

Proof state:
case h.e'_3.h
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ x ∈ P ↔ ∀ (n : ℕ), (C x).coeff n ∈ P

Tactic:
constructor

Result:
case h.e'_3.h.mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ x ∈ P → ∀ (n : ℕ), (C x).coeff n ∈ P

case h.e'_3.h.mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ (∀ (n : ℕ), (C x).coeff n ∈ P) → x ∈ P

Proof state:
case mk.inr.a
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 hf
n : ℕ := Nat.find 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)

Result:
no goals

Proof state:
case h.e'_3.h.mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ (∀ (n : ℕ), (C x).coeff n ∈ P) → x ∈ P

Tactic:
intro h

Result:
case h.e'_3.h.mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : ∀ (n : ℕ), (C x).coeff n ∈ P
⊢ x ∈ P

Proof state:
case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ (map C P).IsPrime

Tactic:
constructor

Result:
case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ map C P ≠ ⊤

case mpr.mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ∀ {x y : R[X]}, x * y ∈ map C P → x ∈ map C P ∨ y ∈ map C P

Proof state:
case h.e'_3.h.mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ x ∈ P → ∀ (n : ℕ), (C x).coeff n ∈ P

Tactic:
rintro h (- | n)

Result:
case h.e'_3.h.mp.zero
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
⊢ (C x).coeff 0 ∈ P

case h.e'_3.h.mp.succ
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
n : ℕ
⊢ (C x).coeff (n + 1) ∈ P

Proof state:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ coeff 1 0 ∉ P

Tactic:
rw [coeff_one_zero, ← eq_top_iff_one]

Result:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤

Proof state:
case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ (map C P).IsPrime → P.IsPrime

Tactic:
intro H

Result:
case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
⊢ P.IsPrime

Proof state:
case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
⊢ P.IsPrime

Tactic:
convert this using 1

Result:
case h.e'_3
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
⊢ P = comap C (map C P)

Proof state:
case mpr.mem_or_mem'.intro
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 hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P

Tactic:
apply mt h.2

Result:
case mpr.mem_or_mem'.intro
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 hf
n : ℕ := Nat.find hg
⊢ ¬(f.coeff (m, n).1 ∈ P ∨ g.coeff (m, n).2 ∈ P)

Proof state:
case mpr.mem_or_mem'.intro
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 hf
n : ℕ := Nat.find hg
⊢ ¬(f.coeff (m, n).1 ∈ P ∨ g.coeff (m, n).2 ∈ P)

Tactic:
rw [not_or]

Result:
case mpr.mem_or_mem'.intro
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 hf
n : ℕ := Nat.find hg
⊢ f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P

Proof state:
case h.e'_3.h.mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : ∀ (n : ℕ), (C x).coeff n ∈ P
⊢ x ∈ P

Tactic:
simpa only [coeff_C_zero] using h 0

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ (map C P).IsPrime ↔ P.IsPrime

Tactic:
constructor

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

case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ P.IsPrime → (map C P).IsPrime

Proof state:
case mpr.mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ ((∃ n, f.coeff n ∉ P) ∧ ∃ n, g.coeff n ∉ P) → ∃ n, (f * g).coeff n ∉ P

Tactic:
rintro ⟨hf, hg⟩

Result:
case mpr.mem_or_mem'.intro
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
⊢ ∃ n, (f * g).coeff n ∉ P

Proof state:
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 hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
⊢ i < m ∨ j < n

Tactic:
omega

Result:
no goals

Proof state:
case mk
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 hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n)
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

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

Result:
case mk
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 hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Proof state:
case mpr.mem_or_mem'.intro
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 hf
n : ℕ := Nat.find hg
⊢ ∃ n, (f * g).coeff n ∉ P

Tactic:
refine ⟨m + n, ?_⟩

Result:
case mpr.mem_or_mem'.intro
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 hf
n : ℕ := Nat.find hg
⊢ (f * g).coeff (m + n) ∉ P

Proof state:
case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ map C P ≠ ⊤

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

Result:
case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ∃ x, coeff 1 x ∉ P

Proof state:
case h.e'_3.h.mp.zero
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
⊢ (C x).coeff 0 ∈ P

Tactic:
rwa [coeff_C_zero]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤

Tactic:
exact h.1

Result:
no goals

Proof state:
case mk.inl
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 hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P

Tactic:
apply P.mul_mem_left

Result:
case mk.inl.a
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 hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 ∈ P

Proof state:
case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
⊢ P.IsPrime

Tactic:
have := comap_isPrime C (map C P)

Result:
case mp
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
⊢ P.IsPrime