-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff [IsPrime I] (hIJ : I ≤ J) {r : S}
    (hr : r ∈ (J : Set S) \ I) {p : R[X]} (p_ne_zero : p.map (Quotient.mk (I.comap f)) ≠ 0)
    (hpI : p.eval₂ f r ∈ I) : ∃ i, p.coeff i ∈ (J.comap f : Set R) \ I.comap f

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
have rbar_ne_zero : Ideal.Quotient.mk I r ≠ 0 := mt (Quotient.mk_eq_zero I).mp hrI

Result:
case intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Proof state:
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
refine ⟨i, (mem_quotient_iff_mem hIJ).mp ?_, mt ?_ ne_zero⟩

Result:
case intro.intro.intro.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ (Quotient.mk I) (f (p.coeff i)) ∈ map (Quotient.mk I) J

case intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ p.coeff i ∈ ↑(comap f I) → (Quotient.mk (comap f I)) (p.coeff i) = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
⊢ eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0

Tactic:
convert Quotient.eq_zero_iff_mem.mpr hpI

Result:
case h.e'_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
⊢ eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    (Quotient.mk I) (eval₂ f r p)

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
obtain ⟨i, ne_zero, mem⟩ :=
  exists_coeff_ne_zero_mem_comap_of_root_mem rbar_ne_zero rbar_mem_J p_ne_zero rbar_root

Result:
case intro.intro.intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Polynomial.map (Quotient.mk (comap f I)) p).coeff i ≠ 0
mem :
  (Polynomial.map (Quotient.mk (comap f I)) p).coeff i ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
hr : r ∈ ↑J \ ↑I
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)

Tactic:
obtain ⟨hrJ, hrI⟩ := hr

Result:
case intro
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
⊢ ∃ i, p.coeff i ∈ ↑(comap f J) \ ↑(comap f I)