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
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)
⊢ 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')

Tactic:
congr_arg (comap · Q') (RingHom.ext fun r => rfl)

Premises used: RingHom.ext, congr_arg, Ideal.comap, 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
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)
⊢ 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')

Tactic:
exact congr_arg (comap · Q') (RingHom.ext fun r => rfl)

Premises used: RingHom.ext, congr_arg, Ideal.comap, 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
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 := 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

Tactic:
_root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 ?_)

Premises used: Iff.mpr, trans, sup_eq_left, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective
-- 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_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)) ⊥ ≤
    P
⊢ 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

Tactic:
refine _root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 ?_)

Premises used: Iff.mpr, trans, sup_eq_left, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective
-- 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 := 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:
simpa [← RingHom.ker_eq_comap_bot] using hIP

Premises used: RingHom.ker_eq_comap_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 : Algebra.IsIntegral R S
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
have :
  ∀ (P' : Ideal S) (hP : P' ≥ I) (hP' : P'.IsPrime) (hP'' : comap (F := R →+* S) (algebraMap R S) P' ≤ 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:
have ⟨P', hP, hP', hP''⟩ := exists_ideal_comap_le_prime P I 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
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (F := R →+* S) (algebraMap R S) P' ≤ P
obtain :
  ∀ (Q : Ideal S) (hQ : Q ≥ P') (hQ' : Q.IsPrime) (hQ'' : comap (F := R →+* S) (algebraMap R S) Q = 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, hQ, hQ', hQ''⟩ := exists_ideal_over_prime_of_isIntegral_of_isPrime P P' hP''

Premises used: Ideal.exists_ideal_over_prime_of_isIntegral_of_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
P : Ideal R
inst_4 : P.IsPrime
I : Ideal S
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (F := R →+* S) (algebraMap R S) P' ≤ P
Q : Ideal S
hQ : Q ≥ P'
hQ' : Q.IsPrime
hQ'' : comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
⟨Q, hP.trans hQ, hQ', hQ''⟩

Premises used: And.intro, Exists.intro, 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
hIP : comap (F := R →+* S) (algebraMap R S) I ≤ P
P' : Ideal S
hP : P' ≥ I
hP' : P'.IsPrime
hP'' : comap (F := R →+* S) (algebraMap R S) P' ≤ P
Q : Ideal S
hQ : Q ≥ P'
hQ' : Q.IsPrime
hQ'' : comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
exact ⟨Q, hP.trans hQ, hQ', hQ''⟩
-- 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 : Algebra R S
inst_3 : IsDomain R
inst_4 : Nontrivial S
inst_5 : Algebra.IsIntegral R S
inst_6 : Module.IsTorsionFree R S
P : Ideal R
inst_7 : P.IsPrime
⊢ comap (F := R →+* S) (algebraMap R S) ⊥ ≤ P

Tactic:
simp
-- 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 : Algebra R S
inst_3 : IsDomain R
inst_4 : Nontrivial S
inst_5 : Algebra.IsIntegral R S
inst_6 : Module.IsTorsionFree R S
P : Ideal R
inst_7 : P.IsPrime
obtain :
  ∀ Q ≥ ⊥,
    ∀ (hQ₁ : Q.IsPrime) (hQ₂ : comap (F := R →+* S) (algebraMap R S) Q = P),
      Nonempty.{u_2 + 1} (↑(P.primesOver S) : Type u_2)
⊢ Nonempty.{u_2 + 1} (↑(P.primesOver S) : Type u_2)

Tactic:
obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_ideal_over_prime_of_isIntegral P (⊥ : Ideal S) (by simp)

Premises used: Bot.bot, Ideal.exists_ideal_over_prime_of_isIntegral
-- 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 : Algebra R S
inst_3 : IsDomain R
inst_4 : Nontrivial S
inst_5 : Algebra.IsIntegral R S
inst_6 : Module.IsTorsionFree R S
P : Ideal R
inst_7 : P.IsPrime
Q : Ideal S
left : Q ≥ ⊥
hQ₁ : Q.IsPrime
hQ₂ : comap (F := R →+* S) (algebraMap R S) Q = P
⊢ Nonempty.{u_2 + 1} (↑(P.primesOver S) : Type u_2)

Tactic:
⟨Q, ⟨hQ₁, (liesOver_iff _ _).mpr hQ₂.symm⟩⟩

Premises used: Iff.mpr, Ideal.liesOver_iff, Nonempty.intro, Subtype.mk, And.intro, 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 : Algebra R S
inst_3 : IsDomain R
inst_4 : Nontrivial S
inst_5 : Algebra.IsIntegral R S
inst_6 : Module.IsTorsionFree R S
P : Ideal R
inst_7 : P.IsPrime
Q : Ideal S
left : Q ≥ ⊥
hQ₁ : Q.IsPrime
hQ₂ : comap (F := R →+* S) (algebraMap R S) Q = P
⊢ Nonempty.{u_2 + 1} (↑(P.primesOver S) : Type u_2)

Tactic:
exact ⟨Q, ⟨hQ₁, (liesOver_iff _ _).mpr hQ₂.symm⟩⟩
-- 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
P_max : P.IsMaximal
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
obtain :
  ∀ (Q : Ideal S) (Q_prime : Q.IsPrime) (hQ : comap (F := R →+* S) (algebraMap R S) Q = P),
    ∃ (Q : Ideal S), Q.IsMaximal ∧ comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ (Q : Ideal S), Q.IsMaximal ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
obtain ⟨Q, -, Q_prime, hQ⟩ := exists_ideal_over_prime_of_isIntegral P ⊥ hP

Premises used: Bot.bot, Ideal.exists_ideal_over_prime_of_isIntegral
-- 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
P_max : P.IsMaximal
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : Q.IsPrime
hQ : comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ (Q : Ideal S), Q.IsMaximal ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
⟨Q, isMaximal_of_isIntegral_of_isMaximal_comap _ (hQ.symm ▸ P_max), hQ⟩

Premises used: And.intro, Exists.intro, 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
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
P : Ideal R
P_max : P.IsMaximal
hP : RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : Q.IsPrime
hQ : comap (F := R →+* S) (algebraMap R S) Q = P
⊢ ∃ (Q : Ideal S), Q.IsMaximal ∧ comap (F := R →+* S) (algebraMap R S) Q = P

Tactic:
exact ⟨Q, isMaximal_of_isIntegral_of_isMaximal_comap _ (hQ.symm ▸ P_max), hQ⟩
-- 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
inst_4 : FaithfulSMul R S
P : Ideal R
inst_5 : P.IsMaximal
simp_rw : ∃ (Q : Ideal S), Q.IsMaximal ∧ under R Q = P
⊢ ∃ (Q : Ideal S), Q.IsMaximal ∧ Q.LiesOver P

Tactic:
simp_rw [liesOver_iff, eq_comm (a := P)]

Premises used: Ideal.liesOver_iff, eq_comm
-- 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
inst_4 : FaithfulSMul R S
P : Ideal R
inst_5 : P.IsMaximal
⊢ RingHom.ker (F := R →+* S) (algebraMap R S) ≤ P

Tactic:
simp [(RingHom.injective_iff_ker_eq_bot _).mp (FaithfulSMul.algebraMap_injective R S)]

Premises used: RingHom.injective_iff_ker_eq_bot, FaithfulSMul.algebraMap_injective, Iff.mp
-- 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
inst_4 : FaithfulSMul R S
P : Ideal R
inst_5 : P.IsMaximal
⊢ ∃ (Q : Ideal S), Q.IsMaximal ∧ under R Q = P

Tactic:
exact exists_ideal_over_maximal_of_isIntegral P (by
    simp [(RingHom.injective_iff_ker_eq_bot _).mp (FaithfulSMul.algebraMap_injective R S)])

Premises used: Ideal.exists_ideal_over_maximal_of_isIntegral
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
mp : Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ → I = ⊤
mpr : I = ⊤ → Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
⊢ Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤

Tactic:
constructor
-- 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
hf₁ : LE.le (α := Ideal R) (RingHom.ker f) ⊤
⊢ Eq.{u_4 + 1} (α := Ideal S) (map (R := R) f ⊤) ⊤

Tactic:
Ideal.map_top _

Premises used: Ideal.map_top
-- 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
hf₁ : LE.le (α := Ideal R) (RingHom.ker f) ⊤
⊢ Eq.{u_4 + 1} (α := Ideal S) (map (R := R) f ⊤) ⊤

Tactic:
exact Ideal.map_top _

Premises used: Ideal.map_top
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
mp : ¬I = ⊤ → ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
⊢ Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ → I = ⊤

Tactic:
contrapose
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
mp : ∀ (m : Ideal R), m.IsMaximal → ∀ (hm : I ≤ m), ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤

Tactic:
obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal I h

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left : m.IsMaximal
hm : I ≤ m
x : Algebra R S := f.toAlgebra
⊢ Algebra.IsIntegral R S

Tactic:
have : Algebra.IsIntegral _ _ := ⟨hf₂⟩
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left : m.IsMaximal
hm : I ≤ m
x : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
mp :
  ∀ (m' : Ideal S),
    m'.IsMaximal →
      IsMaximal (comap (F := R →+* S) (algebraMap R S) m') →
        ∀ (hm : I ≤ comap (F := R →+* S) (algebraMap R S) m'), ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤

Tactic:
obtain ⟨m', _, rfl⟩ := exists_ideal_over_maximal_of_isIntegral m (hf₁.trans hm)

Premises used: Ideal.exists_ideal_over_maximal_of_isIntegral, LE.le.trans, rfl
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left : m'.IsMaximal
left_1 : IsMaximal (comap (F := R →+* S) (algebraMap R S) m')
hm : I ≤ comap (F := R →+* S) (algebraMap R S) m'
⊢ map (F := R →+* S) (algebraMap R S) I ≤ m'

Tactic:
rw [← map_le_iff_le_comap] at hm

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left : m'.IsMaximal
left_1 : IsMaximal (comap (F := R →+* S) (algebraMap R S) m')
hm : map (F := R →+* S) (algebraMap R S) I ≤ m'
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤

Tactic:
(hm.trans_lt (lt_top_iff_ne_top.mpr (IsMaximal.ne_top ‹_›))).ne

Premises used: Iff.mpr, lt_top_iff_ne_top, Ideal.IsMaximal.ne_top, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left : m'.IsMaximal
left_1 : IsMaximal (comap (F := R →+* S) (algebraMap R S) m')
hm : map (F := R →+* S) (algebraMap R S) I ≤ m'
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤

Tactic:
exact (hm.trans_lt (lt_top_iff_ne_top.mpr (IsMaximal.ne_top ‹_›))).ne

Premises used: Iff.mpr, lt_top_iff_ne_top, Ideal.IsMaximal.ne_top, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
I : Ideal R
hf₁ : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf₂ : f.IsIntegral
⊢ RingHom.ker f ≤ I

Tactic:
simp [(RingHom.injective_iff_ker_eq_bot f).mp hf₁]

Premises used: RingHom.injective_iff_ker_eq_bot, Iff.mp
-- 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
simp : ∃ r ∉ p, ∃ (c : S), c * x = (algebraMap R S : (a : R) → S) r
⊢ ∃ r ∉ p, x ∣ (algebraMap R S : (a : R) → S) r

Tactic:
simp only [dvd_def, eq_comm, mul_comm x]

Premises used: dvd_def, eq_comm, mul_comm
-- 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
by_contra! : ∀ (this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r), False
⊢ ∃ r ∉ p, ∃ (c : S), c * x = (algebraMap R S : (a : R) → S) r

Tactic:
by_contra!
-- 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
⊢ Disjoint (↑(span {x}) : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)

Tactic:
simpa [Set.disjoint_iff_forall_ne, Ideal.mem_span_singleton',
      Algebra.algebraMapSubmonoid, @forall_comm S]

Premises used: Ideal.mem_span_singleton', forall_comm, Set.disjoint_iff_forall_ne, Algebra.algebraMapSubmonoid
-- 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
obtain :
  ∀ (Q : Ideal S) (hQ : Q.IsPrime) (hxQ : span {x} ≤ Q)
    (hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)), False
⊢ False

Tactic:
obtain ⟨Q, hQ, hxQ, hQp⟩ := Ideal.exists_le_prime_disjoint (.span {x})
    (Algebra.algebraMapSubmonoid _ p.primeCompl)
    (by simpa [Set.disjoint_iff_forall_ne, Ideal.mem_span_singleton',
      Algebra.algebraMapSubmonoid, @forall_comm S])

Premises used: Ideal.exists_le_prime_disjoint, Ideal.span, Ideal.primeCompl, Algebra.algebraMapSubmonoid, Singleton.singleton
-- 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x_1 : S
hx : x_1 ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x_1 ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ_1 : span {x_1} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
x : R
hxQ : Membership.mem (γ := Submodule R R) (under R Q) x
by_contra : ∀ (hxp : x ∉ p), False
⊢ x ∈ p

Tactic:
by_contra hxp
-- 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x_1 : S
hx : x_1 ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x_1 ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ_1 : span {x_1} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
x : R
hxQ : Membership.mem (γ := Submodule R R) (under R Q) x
hxp : x ∉ p
⊢ False

Tactic:
Set.subset_compl_iff_disjoint_right.mpr hQp hxQ ⟨x, hxp, rfl⟩

Premises used: Iff.mpr, Set.subset_compl_iff_disjoint_right, And.intro, Exists.intro, 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
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x_1 : S
hx : x_1 ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x_1 ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ_1 : span {x_1} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
x : R
hxQ : Membership.mem (γ := Submodule R R) (under R Q) x
hxp : x ∉ p
⊢ False

Tactic:
exact Set.subset_compl_iff_disjoint_right.mpr hQp hxQ ⟨x, hxp, rfl⟩

Premises used: Iff.mpr, Set.subset_compl_iff_disjoint_right, And.intro, Exists.intro, rfl