awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ideal A
inst_4 : I.IsPrime
hI : IsMaximal (comap (F := R →+* A) (algebraMap R A) I)
⊢ I.IsMaximal

Tactic:
isMaximal_of_isIntegral_of_isMaximal_comap I hI

Premises used: Ideal.isMaximal_of_isIntegral_of_isMaximal_comap
-- 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
inst_4 : IsDomain A
inst_5 : Nontrivial R
I : Ideal A
I_ne_bot : I ≠ ⊥
⊢ Ne (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥

Tactic:
let ⟨x, x_mem, x_ne_zero⟩ := I.ne_bot_iff.mp I_ne_bot
  comap_ne_bot_of_integral_mem x_ne_zero x_mem (Algebra.IsIntegral.isIntegral x)

Premises used: Algebra.IsIntegral.isIntegral, Algebra.algebraMap, _private.0.Ideal.IsIntegral.comap_ne_bot.match_1, Ne, Bot.bot, Submodule.ne_bot_iff, Ideal.comap, Iff.mp, Ideal.comap_ne_bot_of_integral_mem
-- 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
inst_4 : IsDomain A
inst_5 : Nontrivial R
I : Ideal A
contrapose : ¬I = ⊥ → ¬Eq (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥
⊢ Eq (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥ → I = ⊥

Tactic:
contrapose
-- 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
inst_4 : IsDomain A
inst_5 : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬Eq (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥

Tactic:
IsIntegral.comap_ne_bot R

Premises used: Ideal.IsIntegral.comap_ne_bot
-- 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
inst_4 : IsDomain A
inst_5 : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬Eq (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥

Tactic:
exact IsIntegral.comap_ne_bot R

Premises used: Ideal.IsIntegral.comap_ne_bot
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
x : R
hx : x ∈ (↑P.primeCompl : Set R)
x0 : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ False

Tactic:
absurd (hP x0) hx

Premises used: absurd
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
x : R
hx : x ∈ (↑P.primeCompl : Set R)
x0 : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ False

Tactic:
exact absurd (hP x0) hx

Premises used: absurd
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
⊢ 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl

Tactic:
have hP0 : (0 : S) ∉ Algebra.algebraMapSubmonoid S P.primeCompl := by
    rintro ⟨x, ⟨hx, x0⟩⟩
    exact absurd (hP x0) hx
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
obtain :
  ∀ (Qₚ : Ideal Sₚ) (Qₚ_maximal : Qₚ.IsMaximal),
    ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
obtain ⟨Qₚ : Ideal Sₚ, Qₚ_maximal⟩ := exists_maximal Sₚ

Premises used: Ideal.exists_maximal, Ideal
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
⊢ Algebra.IsIntegral Rₚ Sₚ

Tactic:
have : Algebra.IsIntegral Rₚ Sₚ := ⟨isIntegral_localization⟩
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
⊢ IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)

Tactic:
have Qₚ_max : IsMaximal (comap _ Qₚ) :=
    isMaximal_comap_of_isIntegral_of_isMaximal (R := Rₚ) (S := Sₚ) Qₚ
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)
⊢ ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
⟨comap (algebraMap S Sₚ) Qₚ, ⟨comap_isPrime _ Qₚ, ?_⟩⟩

Premises used: Algebra.algebraMap, And.intro, Ideal.comap, Exists.intro, Ideal.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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)
refine : comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) Qₚ) = P
⊢ ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
refine ⟨comap (algebraMap S Sₚ) Qₚ, ⟨comap_isPrime _ Qₚ, ?_⟩⟩
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)
⊢ under R (B := Localization (M := R) P.primeCompl) (IsLocalRing.maximalIdeal (Localization (M := R) P.primeCompl)) = P

Tactic:
Localization.AtPrime.under_maximalIdeal (I := P)

Premises used: Localization.AtPrime.under_maximalIdeal
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)
h :
  Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) Qₚ))
    (under R (B := Localization (M := R) P.primeCompl) (IsLocalRing.maximalIdeal (Localization (M := R) P.primeCompl)))
⊢ comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) Qₚ) = P

Tactic:
convert! Localization.AtPrime.under_maximalIdeal (I := P)

Premises used: Localization.AtPrime.under_maximalIdeal
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)
h :
  Eq (α := Ideal R)
    (comap (F := R →+* Sₚ)
      (RingHom.comp
        (IsLocalization.map (M := P.primeCompl) (T := Algebra.algebraMapSubmonoid S P.primeCompl) Sₚ (algebraMap R S) ⋯)
        (algebraMap R Rₚ))
      Qₚ)
    (under R (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ))
⊢ Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) Qₚ))
    (under R (B := Localization (M := R) P.primeCompl) (IsLocalRing.maximalIdeal (Localization (M := R) P.primeCompl)))

Tactic:
rw [comap_comap, ← IsLocalRing.eq_maximalIdeal Qₚ_max,
    ← IsLocalization.map_comp (P := S) (Q := Sₚ) (g := algebraMap R S)
    (M := P.primeCompl) (T := Algebra.algebraMapSubmonoid S P.primeCompl) (S := Rₚ)
    (fun p hp => Algebra.mem_algebraMapSubmonoid_of_mem ⟨p, hp⟩)]

Premises used: IsLocalization.map_comp, Subtype.mk, IsLocalRing.eq_maximalIdeal, Algebra.mem_algebraMapSubmonoid_of_mem, Ideal.comap_comap
-- 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 : IsDomain S
inst_4 : Algebra.IsIntegral R S
P : Ideal R
inst_5 : P.IsPrime
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization (M := R) P.primeCompl
Sₚ : Type u_2 := Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)
this_1 : IsDomain.{u_2} (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl)) := ⋯
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : IsMaximal (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ)
⊢ Eq (α := Ideal R)
    (comap (F := R →+* Sₚ)
      (RingHom.comp
        (IsLocalization.map (M := P.primeCompl) (T := Algebra.algebraMapSubmonoid S P.primeCompl) Sₚ (algebraMap R S) ⋯)
        (algebraMap R Rₚ))
      Qₚ)
    (under R (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ))

Tactic:
rfl
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
⊢ RingHom.ker (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) ≤
    P

Tactic:
simp [hIP]
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
obtain :
  ∀ (Q' : Ideal (S ⧸ I)) (Q'_prime : Q'.IsPrime)
    (hQ' :
      Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
        (comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
        (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
          (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)),
    ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
obtain ⟨Q' : Ideal (S ⧸ I), ⟨Q'_prime, hQ'⟩⟩ :=
    @exists_ideal_over_prime_of_isIntegral_of_isDomain (R ⧸ I.comap (algebraMap R S)) _ (S ⧸ I) _
      Ideal.quotientAlgebra _ _
      (map (Ideal.Quotient.mk (I.comap (algebraMap R S))) P)
      (map_isPrime_of_surjective Quotient.mk_surjective (by simp [hIP]))
      (le_trans (le_of_eq ((RingHom.injective_iff_ker_eq_bot _).1 algebraMap_quotient_injective))
        bot_le)

Premises used: Ideal.algebraMap_quotient_injective, Algebra.algebraMap, Ideal.Quotient.mk, Ideal.map, Ideal, Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain, HasQuotient.Quotient, RingHom.injective_iff_ker_eq_bot, Ideal.comap, Iff.mp, le_of_eq, bot_le, le_trans
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
    (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
⟨Q'.comap _, le_trans (le_of_eq mk_ker.symm) (ker_le_comap _), ⟨comap_isPrime _ Q', ?_⟩⟩

Premises used: Ideal.ker_le_comap, And.intro, Ideal.comap, Exists.intro, Ideal.comap_isPrime, Ideal.mk_ker, le_of_eq, Eq.symm, le_trans
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
    (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)
refine : comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* S ⧸ I) (Quotient.mk I) Q') = P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
refine ⟨Q'.comap _, le_trans (le_of_eq mk_ker.symm) (ker_le_comap _), ⟨comap_isPrime _ Q', ?_⟩⟩
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
    (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)
rw : comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q' = P
⊢ comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* S ⧸ I) (Quotient.mk I) Q') = P

Tactic:
rw [comap_comap]

Premises used: Ideal.comap_comap
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
    (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)
⊢ comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q' = P

Tactic:
_root_.trans ?_ (_root_.trans (congr_arg (comap (Ideal.Quotient.mk
    (comap (algebraMap R S) I))) hQ') ?_)

Premises used: trans, Algebra.algebraMap, Ideal.Quotient.mk, congr_arg, Ideal.comap
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
    (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)
refine_1 :
  Eq (α := Ideal R) (comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q')
    (comap (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I))
      (comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q'))
refine_2 :
  comap (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I))
      (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
        (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P) =
    P
⊢ comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q' = P

Tactic:
refine _root_.trans ?_ (_root_.trans (congr_arg (comap (Ideal.Quotient.mk
    (comap (algebraMap R S) I))) hQ') ?_)

Premises used: trans, Algebra.algebraMap, Ideal.Quotient.mk, congr_arg, Ideal.comap
-- 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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
inst_5 : I.IsPrime
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' :
  Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q')
    (map (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)) P)
refine_1 :
  Eq (α := Ideal R) (comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q')
    (comap (F := RingHom.{u_1, u_2} R (S ⧸ I))
      (RingHom.comp (β := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
        (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I)))
      Q')
⊢ Eq (α := Ideal R) (comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q')
    (comap (F := R →+* HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
      (Quotient.mk (comap (F := R →+* S) (algebraMap R S) I))
      (comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I)) (S ⧸ I)) Q'))

Tactic:
rw [comap_comap]

Premises used: Ideal.comap_comap