awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_zero₁ :
  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))
⊢ Membership.mem (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (γ :=
    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))
    ((Quotient.mk (comap f I) : (a : R) → R ⧸ comap f I) (p.coeff i) :
      HasQuotient.Quotient R (B := Ideal R) (comap f I))

Tactic:
rw [coeff_map] at ne_zero mem

Premises used: Polynomial.coeff_map
-- 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))
    ((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))
mem :
  Membership.mem (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (γ :=
    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))
    ((Quotient.mk (comap f I) : (a : R) → R ⧸ comap f I) (p.coeff i) :
      HasQuotient.Quotient R (B := Ideal R) (comap f I))
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)

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

Premises used: mt, Ideal.mem_quotient_iff_mem, And.intro, Exists.intro, Iff.mp
-- 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))
    ((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))
mem :
  Membership.mem (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (γ :=
    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))
    ((Quotient.mk (comap f I) : (a : R) → R ⧸ comap f I) (p.coeff i) :
      HasQuotient.Quotient R (B := Ideal R) (comap f I))
refine_1 :
  Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) ((f : (a : R) → S) (p.coeff i)) : S ⧸ I)
refine_2 :
  p.coeff i ∈ (↑(comap f I) : Set R) →
    Eq (α := 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))
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)

Tactic:
refine ⟨i, (mem_quotient_iff_mem hIJ).mp ?_, mt ?_ ne_zero⟩
-- 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))
    ((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))
mem :
  Membership.mem (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (γ :=
    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))
    ((Quotient.mk (comap f I) : (a : R) → R ⧸ comap f I) (p.coeff i) :
      HasQuotient.Quotient R (B := Ideal R) (comap f I))
⊢ Membership.mem (α := S ⧸ I) (γ := Ideal (S ⧸ I)) (map (F := S →+* S ⧸ I) (Quotient.mk I) J)
    ((Quotient.mk I : (a : S) → S ⧸ I) ((f : (a : R) → S) (p.coeff i)) : S ⧸ I)

Tactic:
simpa using 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))
    ((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))
mem :
  Membership.mem (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (γ :=
    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))
    ((Quotient.mk (comap f I) : (a : R) → R ⧸ comap f I) (p.coeff i) :
      HasQuotient.Quotient R (B := Ideal R) (comap f I))
⊢ p.coeff i ∈ (↑(comap f I) : Set R) →
    Eq (α := 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:
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
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
hp : eval₂ f r p ∈ I
⊢ LT.lt (α := Ideal R) (comap f I) (comap f J)

Tactic:
let ⟨i, hJ, hI⟩ := exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff hIJ hr p_ne_zero hp
  SetLike.lt_iff_le_and_exists.mpr ⟨comap_mono hIJ, p.coeff i, hJ, hI⟩

Premises used: Iff.mpr, SetLike.lt_iff_le_and_exists, Ideal.comap_mono, Polynomial.coeff, Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff, _private.0.Ideal.comap_lt_comap_of_root_mem_sdiff.match_1, And.intro, LT.lt, Ideal.comap, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
h : 1 ∈ I
x : S
⊢ x ∈ I

Tactic:
(I.eq_top_iff_one.mpr h).symm ▸ mem_top

Premises used: Iff.mpr, Eq.rec, Ideal.eq_top_iff_one, Eq.symm, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I J : Ideal S
inst_2 : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ (↑J : Set S) \ (↑I : Set S)
integral : IsIntegral R x
obtain :
  ∀ (p : R[X]) (p_monic : p.Monic) (hpx : eval₂ (algebraMap R S) x p = 0),
    LT.lt (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) (comap (F := R →+* S) (algebraMap R S) J)
⊢ LT.lt (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) (comap (F := R →+* S) (algebraMap R S) J)

Tactic:
obtain ⟨p, p_monic, hpx⟩ := integral
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I J : Ideal S
inst_2 : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ LT.lt (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) (comap (F := R →+* S) (algebraMap R S) J)

Tactic:
comap_lt_comap_of_root_mem_sdiff hIJ mem (map_monic_ne_zero p_monic) ?_

Premises used: Polynomial.map_monic_ne_zero, Ideal.comap_lt_comap_of_root_mem_sdiff
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I J : Ideal S
inst_2 : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
refine : eval₂ (algebraMap R S) x p ∈ I
⊢ LT.lt (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) (comap (F := R →+* S) (algebraMap R S) J)

Tactic:
refine comap_lt_comap_of_root_mem_sdiff hIJ mem (map_monic_ne_zero p_monic) ?_

Premises used: Polynomial.map_monic_ne_zero, Ideal.comap_lt_comap_of_root_mem_sdiff
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I J : Ideal S
inst_2 : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ 0 ∈ I

Tactic:
I.zero_mem

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I J : Ideal S
inst_2 : Algebra R S
hI : I.IsPrime
hIJ : I ≤ J
x : S
mem : x ∈ (↑J : Set S) \ (↑I : Set S)
p : R[X]
p_monic : p.Monic
hpx : eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x p ∈ I

Tactic:
convert! I.zero_mem

Premises used: Ideal.zero_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 : Ideal S
inst_2 : IsDomain S
r : S
r_ne_zero : r ≠ 0
hr : r ∈ I
p : R[X]
p_ne_zero : p ≠ 0
hp : eval₂ f r p = 0
⊢ Ne (α := Ideal R) (comap f I) ⊥

Tactic:
fun h =>
  let ⟨_, hi, mem⟩ := exists_coeff_ne_zero_mem_comap_of_root_mem r_ne_zero hr p_ne_zero hp
  absurd (mem_bot.mp (eq_bot_iff.mp h mem)) hi

Premises used: Ideal.mem_bot, False, absurd, Iff.mp, Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem, eq_bot_iff, _private.0.Ideal.comap_ne_bot_of_root_mem.match_1, Not
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal S
inst_4 : I.IsPrime
hI : IsMaximal (comap (F := R →+* S) (algebraMap R S) I)
⊢ I.IsMaximal

Tactic:
⟨⟨mt comap_eq_top_iff.mpr hI.1.1, fun _ I_lt_J =>
      let ⟨I_le_J, x, hxJ, hxI⟩ := SetLike.lt_iff_le_and_exists.mp I_lt_J
      comap_eq_top_iff.1 <|
        hI.1.2 _ (comap_lt_comap_of_integral_mem_sdiff I_le_J ⟨hxJ, hxI⟩
          (Algebra.IsIntegral.isIntegral x))⟩⟩

Premises used: Iff.mpr, SetLike.lt_iff_le_and_exists, Algebra.IsIntegral.isIntegral, Algebra.algebraMap, Ideal.comap_eq_top_iff, mt, Ideal.IsMaximal.mk, Ideal.comap_lt_comap_of_integral_mem_sdiff, And.right, Ideal.IsMaximal.out, And.left, And.intro, Ideal.comap, Iff.mp, _private.0.Ideal.isMaximal_of_isIntegral_of_isMaximal_comap.match_1, Top.top, Eq
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
I : Ideal S
inst_2 : I.IsPrime
hI : IsMaximal (comap f I)
⊢ I.IsMaximal

Tactic:
let _ : Algebra R S := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  isMaximal_of_isIntegral_of_isMaximal_comap (R := R) (S := S) I hI

Premises used: Algebra.IsIntegral.mk, RingHom.toAlgebra, Ideal.isMaximal_of_isIntegral_of_isMaximal_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : IsDomain S
x : S
x_ne_zero : x ≠ 0
x_mem : x ∈ I
hx : IsAlgebraic R x
⊢ Ne (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥

Tactic:
let ⟨_, p_ne_zero, hp⟩ := hx
  comap_ne_bot_of_root_mem x_ne_zero x_mem p_ne_zero hp

Premises used: Algebra.algebraMap, Ne, Bot.bot, Ideal.comap_ne_bot_of_root_mem, _private.0.Ideal.comap_ne_bot_of_algebraic_mem.match_1, Ideal.comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
x : S
x_ne_zero : x ≠ 0
x_mem : x ∈ I
hx : IsIntegral R x
⊢ Ne (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥

Tactic:
comap_ne_bot_of_algebraic_mem x_ne_zero x_mem hx.isAlgebraic

Premises used: Ideal.comap_ne_bot_of_algebraic_mem, IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
⊢ I = ⊥

Tactic:
eq_bot_iff.2 fun x hx => ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
refine : ∀ (x : S) (hx : x ∈ I), Membership.mem (γ := Submodule S S) ⊥ x
⊢ I = ⊥

Tactic:
refine eq_bot_iff.2 fun x hx => ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
x : S
hx : x ∈ I
pos : ∀ (hx0 : x = 0), Membership.mem (γ := Submodule S S) ⊥ x
neg : ∀ (hx0 : ¬x = 0), Membership.mem (γ := Submodule S S) ⊥ x
⊢ Membership.mem (γ := Submodule S S) ⊥ x

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ Membership.mem (γ := Submodule S S) ⊥ x

Tactic:
hx0.symm ▸ Ideal.zero_mem ⊥

Premises used: Eq.rec, Bot.bot, Ideal.zero_mem, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
x : S
hx : x ∈ I
hx0 : x = 0
⊢ Membership.mem (γ := Submodule S S) ⊥ x

Tactic:
exact hx0.symm ▸ Ideal.zero_mem ⊥
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ Membership.mem (γ := Submodule S S) ⊥ x

Tactic:
absurd hI (comap_ne_bot_of_integral_mem hx0 hx (Algebra.IsIntegral.isIntegral x))

Premises used: Algebra.IsIntegral.isIntegral, absurd, Ideal.comap_ne_bot_of_integral_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
I : Ideal S
inst_2 : Algebra R S
inst_3 : Nontrivial R
inst_4 : IsDomain S
inst_5 : Algebra.IsIntegral R S
hI : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) ⊥
x : S
hx : x ∈ I
hx0 : ¬x = 0
⊢ Membership.mem (γ := Submodule S S) ⊥ x

Tactic:
exact absurd hI (comap_ne_bot_of_integral_mem hx0 hx (Algebra.IsIntegral.isIntegral x))

Premises used: Algebra.IsIntegral.isIntegral, absurd, Ideal.comap_ne_bot_of_integral_mem
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ IsMaximal (comap (F := R →+* S) (algebraMap R S) I)

Tactic:
Ideal.Quotient.maximal_of_isField _ ?_

Premises used: Ideal.Quotient.maximal_of_isField
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
refine : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
⊢ IsMaximal (comap (F := R →+* S) (algebraMap R S) I)

Tactic:
refine Ideal.Quotient.maximal_of_isField _ ?_

Premises used: Ideal.Quotient.maximal_of_isField
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ IsPrime (comap (F := R →+* S) (algebraMap R S) I)

Tactic:
haveI : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : IsPrime (comap (F := R →+* S) (algebraMap R S) I)
rwa rwa₁ rwa₂ rwa₃ : I.IsMaximal
⊢ IsField.{u_2} (S ⧸ I)

Tactic:
rwa [← Quotient.maximal_ideal_iff_isField_quotient]

Premises used: Ideal.Quotient.maximal_ideal_iff_isField_quotient
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : IsPrime (comap (F := R →+* S) (algebraMap R S) I)
⊢ IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))

Tactic:
exact isField_of_isIntegral_of_isField
    algebraMap_quotient_injective (by rwa [← Quotient.maximal_ideal_iff_isField_quotient])

Premises used: isField_of_isIntegral_of_isField
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsIntegral
I : Ideal S
inst_2 : I.IsMaximal
⊢ IsMaximal (comap f I)

Tactic:
let _ : Algebra R S := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  isMaximal_comap_of_isIntegral_of_isMaximal (R := R) (S := S) I

Premises used: Ideal.isMaximal_comap_of_isIntegral_of_isMaximal, Algebra.IsIntegral.mk, RingHom.toAlgebra
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
A : Type u_3
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Algebra.IsIntegral R A
I J : Ideal A
inst_4 : I.IsPrime
I_lt_J : I < J
⊢ LT.lt (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) (comap (F := R →+* A) (algebraMap R A) J)

Tactic:
let ⟨I_le_J, x, hxJ, hxI⟩ := SetLike.lt_iff_le_and_exists.mp I_lt_J
  comap_lt_comap_of_integral_mem_sdiff I_le_J ⟨hxJ, hxI⟩ (Algebra.IsIntegral.isIntegral x)

Premises used: SetLike.lt_iff_le_and_exists, Algebra.IsIntegral.isIntegral, Algebra.algebraMap, Ideal.comap_lt_comap_of_integral_mem_sdiff, And.intro, LT.lt, Ideal.comap, Iff.mp, _private.0.Ideal.isMaximal_of_isIntegral_of_isMaximal_comap.match_1