awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
have refine : comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* S ⧸ I) (Quotient.mk I) Q') = P
Tactic: refine ⟨Q'.comap _, le_trans (le_of_eq mk_ker.symm) (ker_le_comap _), ⟨comap_isPrime _ Q', ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 →+* S) (algebraMap R S) (comap (F := S →+* S ⧸ I) (Quotient.mk I) Q') = P
have rw : comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q' = P
Tactic: rw [comap_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
have 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'))
Tactic: refine _root_.trans ?_ (_root_.trans (congr_arg (comap (Ideal.Quotient.mk
    (comap (algebraMap R S) I))) hQ') ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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'))
⊢ comap (F := RingHom.{u_1, u_2} R (S ⧸ I)) (RingHom.comp (Quotient.mk I) (algebraMap R S)) Q' = P
have 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
Tactic: refine _root_.trans ?_ (_root_.trans (congr_arg (comap (Ideal.Quotient.mk
    (comap (algebraMap R S) I))) hQ') ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 := 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'))
have 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')
Tactic: rw [comap_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
have 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
Tactic: refine _root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ ∃ Q ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have 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
Tactic: have ⟨P', hP, hP', hP''⟩ := exists_ideal_comap_le_prime P I hIP
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 ≥ I, Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have 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
Tactic: obtain ⟨Q, hQ, hQ', hQ''⟩ := exists_ideal_over_prime_of_isIntegral_of_isPrime P P' hP''
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ Nonempty.{u_2 + 1} (↑(P.primesOver S) : Type u_2)
have 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)
Tactic: obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_ideal_over_prime_of_isIntegral P (⊥ : Ideal S) (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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.IsMaximal ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have 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
Tactic: obtain ⟨Q, -, Q_prime, hQ⟩ := exists_ideal_over_prime_of_isIntegral P ⊥ hP
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 ∧ Q.LiesOver P
have simp_rw : ∃ (Q : Ideal S), Q.IsMaximal ∧ under R Q = P
Tactic: simp_rw [liesOver_iff, eq_comm (a := P)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤
have mp : Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ → I = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 = ⊤
⊢ Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤
have mpr : I = ⊤ → Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤ → I = ⊤
have mp : ¬I = ⊤ → ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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 = ⊤
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
have mp : ∀ (m : Ideal R), m.IsMaximal → ∀ (hm : I ≤ m), ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
Tactic: obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal I h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
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
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
have this : Algebra.IsIntegral R S
Tactic: have : Algebra.IsIntegral _ _ := ⟨hf₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
have 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) ⊤
Tactic: obtain ⟨m', _, rfl⟩ := exists_ideal_over_maximal_of_isIntegral m (hf₁.trans hm)
Cleared hypotheses: m, left, hm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
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'
⊢ ¬Eq.{u_4 + 1} (α := Ideal S) (map f I) ⊤
have hm₁ : map (F := R →+* S) (algebraMap R S) I ≤ m'
Tactic: rw [← map_le_iff_le_comap] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ ∃ r ∉ p, x ∣ (algebraMap R S : (a : R) → S) r
have simp : ∃ r ∉ p, ∃ (c : S), c * x = (algebraMap R S : (a : R) → S) r
Tactic: simp only [dvd_def, eq_comm, mul_comm x]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ ∃ r ∉ p, ∃ (c : S), c * x = (algebraMap R S : (a : R) → S) r
have by_contra! : ∀ (this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ False
have obtain : ∀ (Q : Ideal S) (hQ : Q.IsPrime) (hxQ : span {x} ≤ Q)
  (hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)), 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])
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ x ∈ p
have by_contra : ∀ (hxp : x ∉ p), False
Tactic: by_contra hxp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
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
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
⊢ False
have hQp' : under R Q ≤ p
Tactic: have hQp' : Q.under _ ≤ p := by
    intro x hxQ
    by_contra hxp
    exact Set.subset_compl_iff_disjoint_right.mpr hQp hxQ ⟨x, hxp, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
⊢ False
have obtain : ∀ (Q' : Ideal S) (hQ'Q : Q' ≥ Q) (hQ' : Q'.IsPrime) (hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p), False
Tactic: obtain ⟨Q', hQ'Q, hQ', hQ'p⟩ := Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime _ _ hQp'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst_1 : CommRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_6 : 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
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
inst : Q'.IsPrime
⊢ False
have hq₁ : Eq (α := Set (Ideal S)) (p.primesOver S) {Q'}
Tactic: obtain rfl : Q' = q := hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩
Cleared hypotheses: q, inst_5, hq, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
R : Type u_1
inst_1 : CommRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_6 : 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
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
inst : Q'.IsPrime
hq₁ : Eq (α := Set (Ideal S)) (p.primesOver S) {Q'}
⊢ False
have hx₁ : x ∉ Q'
Tactic: obtain rfl : Q' = q := hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩
Cleared hypotheses: q, inst_5, hq, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
hpm : p.IsMaximal
inst_5 : P.IsPrime
⊢ P.IsMaximal
have hpm₁ : IsMaximal (Ideal.under A P)
Tactic: rw [P.over_def p] at hpm
Cleared hypotheses: hpm, inst_5
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
inst_5 : P.IsMaximal
⊢ p.IsMaximal
have rw : IsMaximal (Ideal.under A P)
Tactic: rw [P.over_def p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
⊢ Eq (α := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) {⊥}
have h : ∀ (p : Ideal B),
  Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p ↔ Membership.mem (γ := Set (Ideal B)) {⊥} p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
p : Ideal B
⊢ Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p ↔ Membership.mem (γ := Set (Ideal B)) {⊥} p
have h : Membership.mem (γ := Set (Ideal B)) {⊥} p → Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p
Tactic: refine ⟨fun ⟨_, ⟨h⟩⟩ ↦ p.eq_bot_of_comap_eq_bot h.symm, ?_⟩