case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
⊢ ∃ p, p ∈ P ∧ Polynomial.map (Quotient.mk (comap C P)) p ≠ 0
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
⊢ ∃ p, p ∈ P ∧ Polynomial.map (Quotient.mk (comap C P)) p ≠ 0
obtain ⟨m, hm⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb)
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ ↑m = 0
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
⊢ ∃ p, p ∈ P ∧ Polynomial.map (Quotient.mk (comap C P)) p ≠ 0
refine' ⟨m, Submodule.coe_mem m, fun pp0 => hm (Submodule.coe_eq_zero.mp _)⟩
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ Function.Injective ↑(mapRingHom (Quotient.mk (comap C P)))
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ ↑m = 0
refine'
  (injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk
    (P.comap (C : R →+* R[X]))))).mp
    _ _ pp0
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ RingHom.ker (Quotient.mk (comap C P)) = ⊥
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ Function.Injective ↑(mapRingHom (Quotient.mk (comap C P)))
refine' map_injective _ ((Ideal.Quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr _)
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ comap C P = ⊥
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ RingHom.ker (Quotient.mk (comap C P)) = ⊥
rw [mk_ker]
no goals
case intro
R : Type u_1
inst✝¹ : CommRing R
S : Type ?u.73967
inst✝ : CommRing S
f : R →+* S
I J : Ideal S
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), ↑C x ∈ P → x = 0
m : { x // x ∈ P }
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ comap C P = ⊥
exact (Submodule.eq_bot_iff _).mpr fun x hx => hP x (mem_comap.mp hx)