awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
x : R
⊢ Eq (α :=
    HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
      Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
    ((@RingHom.comp _ (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) _ _
            Semiring.toNonAssocSemiring _
            (RingHom.comp
              (Quotient.mk
                (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
                  (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
              C)
            (Quotient.mk (comap (F := R →+* R[X]) C P)) :
          (a : R) → (R ⧸ comap C P)[X] ⧸ map (mapRingHom (Quotient.mk (comap C P))) P)
        x :
      HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
        Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (quotientMap
              (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
                (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P)
              (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⋯)
            (RingHom.comp (Quotient.mk P) C) :
          (a : R) → (R ⧸ comap C P)[X] ⧸ map (mapRingHom (Quotient.mk (comap C P))) P)
        x :
      HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
        Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
obtain :
  ∀ (m : ↥P) (hm : m ≠ 0),
    ∃ p ∈ P,
      Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
⊢ ∃ p ∈ P,
    Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0

Tactic:
obtain ⟨m, hm⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb)

Premises used: Iff.mpr, Submodule.nonzero_mem_of_bot_lt, bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
⊢ ∃ p ∈ P,
    Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0

Tactic:
⟨m, Submodule.coe_mem m, fun pp0 => hm (Submodule.coe_eq_zero.mp ?_)⟩

Premises used: Submodule.coe_mem, And.intro, Exists.intro, Iff.mp, Submodule.coe_eq_zero, Subtype.val
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
refine :
  ∀
    (pp0 :
      Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0),
    (↑m : R[X]) = 0
⊢ ∃ p ∈ P,
    Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0

Tactic:
refine ⟨m, Submodule.coe_mem m, fun pp0 => hm (Submodule.coe_eq_zero.mp ?_)⟩
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ (↑m : R[X]) = 0

Tactic:
(injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk
      (P.comap (C : R →+* R[X]))))).mp
      ?_ _ pp0

Premises used: Polynomial.C, Ideal.Quotient.mk, injective_iff_map_eq_zero, Polynomial.mapRingHom, Ideal.comap, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
R₁ :
  Function.Injective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (⇑(mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) : (a : R[X]) → (R ⧸ comap C P)[X])
⊢ (↑m : R[X]) = 0

Tactic:
refine
    (injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk
      (P.comap (C : R →+* R[X]))))).mp
      ?_ _ pp0

Premises used: Polynomial.C, Ideal.Quotient.mk, injective_iff_map_eq_zero, Polynomial.mapRingHom, Ideal.comap, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ Function.Injective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (⇑(mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) : (a : R[X]) → (R ⧸ comap C P)[X])

Tactic:
map_injective _ ((RingHom.injective_iff_ker_eq_bot (Ideal.Quotient.mk (P.comap C))).mpr ?_)

Premises used: Iff.mpr, Polynomial.C, Ideal.Quotient.mk, Polynomial.map_injective, RingHom.injective_iff_ker_eq_bot, Ideal.comap, Polynomial.map
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
refine :
  Eq (α := Ideal R)
    (RingHom.ker (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
      (Quotient.mk (comap (F := R →+* R[X]) C P)))
    ⊥
⊢ Function.Injective (α := R[X]) (β := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (⇑(mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) : (a : R[X]) → (R ⧸ comap C P)[X])

Tactic:
refine map_injective _ ((RingHom.injective_iff_ker_eq_bot (Ideal.Quotient.mk (P.comap C))).mpr ?_)

Premises used: Iff.mpr, Polynomial.C, Ideal.Quotient.mk, Polynomial.map_injective, RingHom.injective_iff_ker_eq_bot, Ideal.comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
rw : Eq (α := Ideal R) (comap (F := R →+* R[X]) C P) ⊥
⊢ Eq (α := Ideal R)
    (RingHom.ker (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
      (Quotient.mk (comap (F := R →+* R[X]) C P)))
    ⊥

Tactic:
rw [mk_ker]

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ Eq (α := Ideal R) (comap (F := R →+* R[X]) C P) ⊥

Tactic:
(Submodule.eq_bot_iff _).mpr fun x hx => hP x (mem_comap.mp hx)

Premises used: Iff.mpr, Iff.mp, Submodule.eq_bot_iff, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
m : ↥P
hm : m ≠ 0
pp0 :
  Eq (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (Polynomial.map (Quotient.mk (comap (F := R →+* R[X]) C P)) (↑m : R[X])) 0
⊢ Eq (α := Ideal R) (comap (F := R →+* R[X]) C P) ⊥

Tactic:
exact (Submodule.eq_bot_iff _).mpr fun x hx => hP x (mem_comap.mp hx)

Premises used: Iff.mpr, Iff.mp, Submodule.eq_bot_iff, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
inst_2 : IsDomain S
r : S
r_ne_zero : r ≠ 0
hr : r ∈ I
p : R[X]
⊢ p ≠ 0 → eval₂ f r p = 0 → ∃ (i : ℕ), p.coeff i ≠ 0 ∧ Membership.mem (γ := Ideal R) (comap f I) (p.coeff i)

Tactic:
exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem
    (fun {_} h => Or.resolve_right (mul_eq_zero.mp h) r_ne_zero) hr

Premises used: mul_eq_zero, Iff.mp, Or.resolve_right, Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
hr : r ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
⊢ r ∈ (↑J : Set S)

Tactic:
obtain ⟨hrJ, hrI⟩ := hr
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
hr : r ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
⊢ r ∉ (↑I : Set S)

Tactic:
obtain ⟨hrJ, hrI⟩ := hr
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
⊢ Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)

Tactic:
have rbar_ne_zero : Ideal.Quotient.mk I r ≠ 0 := mt (Quotient.mk_eq_zero I).mp hrI
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
⊢ Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)

Tactic:
have rbar_mem_J : Ideal.Quotient.mk I r ∈ J.map (Ideal.Quotient.mk I) := mem_map_of_mem _ hrJ
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
⊢ ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)

Tactic:
simp [Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
⊢ ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)

Tactic:
have quotient_f : ∀ x ∈ I.comap f, (Ideal.Quotient.mk I).comp f x = 0 := by
    simp [Quotient.eq_zero_iff_mem]
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
⊢ Eq (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) (eval₂ f r p) : S ⧸ I) (0 : S ⧸ I)

Tactic:
Quotient.eq_zero_iff_mem.mpr hpI

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
h :
  eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    (Quotient.mk I : (a : S) → S ⧸ I) (eval₂ f r p)
⊢ eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0

Tactic:
convert! Quotient.eq_zero_iff_mem.mpr hpI

Premises used: Iff.mpr, Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
⊢ eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    (Quotient.mk I : (a : S) → S ⧸ I) (eval₂ f r p)

Tactic:
_root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm

Premises used: trans, Ideal.Quotient.mk, Polynomial.hom_eval₂, Polynomial.eval₂_map, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
⊢ eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    (Quotient.mk I : (a : S) → S ⧸ I) (eval₂ f r p)

Tactic:
exact _root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm

Premises used: trans, Ideal.Quotient.mk, Polynomial.hom_eval₂, Polynomial.eval₂_map, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
⊢ eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0

Tactic:
have rbar_root :
    (p.map (Ideal.Quotient.mk (I.comap f))).eval₂ (Quotient.lift (I.comap f) _ quotient_f)
        (Ideal.Quotient.mk I r) =
      0 := by
    convert! Quotient.eq_zero_iff_mem.mpr hpI
    exact _root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
rbar_root :
  eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
obtain :
  ∀ (i : ℕ)
    (ne_zero :
      Ne (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (coeff (Polynomial.map (Quotient.mk (comap f I)) p) i)
        0)
    (mem :
      Membership.mem (γ := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap f I)))
        (comap (F := RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap f I)) (S ⧸ I))
          (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f)
          (map (F := S →+* S ⧸ I) (Quotient.mk I) J))
        (coeff (Polynomial.map (Quotient.mk (comap f I)) p) i)),
    ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)

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

Premises used: Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I J : Ideal S
inst_2 : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap f I))[X]) (Polynomial.map (Quotient.mk (comap f I)) p) 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ (↑J : Set S)
hrI : r ∉ (↑I : Set S)
rbar_ne_zero : Ne (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I) (0 : S ⧸ I)
rbar_mem_J :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) r : S ⧸ I)
quotient_f :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (comap f I) x →
      Eq.{u_2 + 1} (α := S ⧸ I)
        (((RingHom.comp (Quotient.mk I) f : RingHom.{u_1, u_2} R (S ⧸ I)) : (a : R) → S ⧸ I) x : S ⧸ I) (0 : S ⧸ I)
rbar_root :
  eval₂ (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f) ((Quotient.mk I : (a : S) → S ⧸ I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero :
  Ne (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (coeff (Polynomial.map (Quotient.mk (comap f I)) p) i) 0
mem :
  Membership.mem (γ := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap f I)))
    (comap (F := RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap f I)) (S ⧸ I))
      (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f)
      (map (F := S →+* S ⧸ I) (Quotient.mk I) J))
    (coeff (Polynomial.map (Quotient.mk (comap f I)) p) i)
⊢ Ne (α := HasQuotient.Quotient R (B := Ideal R) (comap f I))
    ((Quotient.mk (comap f I) : (a : R) → R ⧸ comap f I) (p.coeff i) :
      HasQuotient.Quotient R (B := Ideal R) (comap f I))
    (0 : HasQuotient.Quotient R (B := Ideal R) (comap f I))

Tactic:
rw [coeff_map] at ne_zero mem

Premises used: Polynomial.coeff_map