awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have 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
Tactic: have rbar_root :
    (p.map (Ideal.Quotient.mk (I.comap f))).eval₂ (Quotient.lift (I.comap f) _ quotient_f)
        (Ideal.Quotient.mk I r) =
      0 := by
    convert! Quotient.eq_zero_iff_mem.mpr hpI
    exact _root_.trans (eval₂_map _ _ _) (hom_eval₂ p f (Ideal.Quotient.mk I) r).symm
-- 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 : 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 : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have obtain : ∀ (i : ℕ)
  (ne_zero :
    Ne (α := HasQuotient.Quotient R (B := Ideal R) (comap f I)) (coeff (Polynomial.map (Quotient.mk (comap f I)) p) i)
      0)
  (mem :
    Membership.mem (γ := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap f I)))
      (comap (F := RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap f I)) (S ⧸ I))
        (Quotient.lift (comap f I) (RingHom.comp (Quotient.mk I) f) quotient_f)
        (map (F := S →+* S ⧸ I) (Quotient.mk I) J))
      (coeff (Polynomial.map (Quotient.mk (comap f I)) p) i)),
  ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
Tactic: obtain ⟨i, ne_zero, mem⟩ :=
    exists_coeff_ne_zero_mem_comap_of_root_mem rbar_ne_zero rbar_mem_J p_ne_zero rbar_root
-- 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
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)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have 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))
Tactic: rw [coeff_map] at ne_zero mem
Cleared hypotheses: ne_zero, mem
-- 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
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))
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have 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))
Tactic: rw [coeff_map] at ne_zero mem
Cleared hypotheses: ne_zero, mem
-- 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 : 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)
have 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)
Tactic: refine ⟨i, (mem_quotient_iff_mem hIJ).mp ?_, mt ?_ ne_zero⟩
-- 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 : 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)
⊢ ∃ (i : ℕ), p.coeff i ∈ (↑(comap f J) : Set R) \ (↑(comap f I) : Set R)
have 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))
Tactic: refine ⟨i, (mem_quotient_iff_mem hIJ).mp ?_, mt ?_ ne_zero⟩
-- 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
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
⊢ LT.lt (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) I) (comap (F := R →+* S) (algebraMap R S) J)
have 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)
Tactic: obtain ⟨p, p_monic, hpx⟩ := integral
Cleared hypotheses: integral
-- 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
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)
have refine : eval₂ (algebraMap R S) x p ∈ I
Tactic: refine comap_lt_comap_of_root_mem_sdiff hIJ mem (map_monic_ne_zero p_monic) ?_
-- 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
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 = ⊥
have refine : ∀ (x : S) (hx : x ∈ I), Membership.mem (γ := Submodule S S) ⊥ x
Tactic: refine eq_bot_iff.2 fun x hx => ?_
-- 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
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
⊢ Membership.mem (γ := Submodule S S) ⊥ x
have pos : ∀ (hx0 : x = 0), Membership.mem (γ := Submodule S S) ⊥ x
Tactic: by_cases hx0 : x = 0
-- 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
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
⊢ Membership.mem (γ := Submodule S S) ⊥ x
have neg : ∀ (hx0 : ¬x = 0), Membership.mem (γ := Submodule S S) ⊥ x
Tactic: by_cases hx0 : x = 0
-- 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
I : Ideal S
hI : I.IsMaximal
⊢ IsMaximal (comap (F := R →+* S) (algebraMap R S) I)
have refine : IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
Tactic: refine Ideal.Quotient.maximal_of_isField _ ?_
-- 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
inst_3 : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ IsField.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) I))
have this : IsPrime (comap (F := R →+* S) (algebraMap R S) I)
Tactic: haveI : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
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
⊢ Eq (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥ → I = ⊥
have contrapose : ¬I = ⊥ → ¬Eq (α := Ideal R) (comap (F := R →+* A) (algebraMap R A) I) ⊥
Tactic: contrapose
-- 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
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
⊢ ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have hP0 : 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
-- 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 : 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.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have obtain : ∀ (Qₚ : Ideal Sₚ) (Qₚ_maximal : Qₚ.IsMaximal), ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
Tactic: obtain ⟨Qₚ : Ideal Sₚ, Qₚ_maximal⟩ := exists_maximal Sₚ
-- 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
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
⊢ ∃ (Q : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have this₁ : Algebra.IsIntegral Rₚ Sₚ
Tactic: have : Algebra.IsIntegral Rₚ Sₚ := ⟨isIntegral_localization⟩
-- 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
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 : Ideal S), Q.IsPrime ∧ comap (F := R →+* S) (algebraMap R S) Q = P
have Qₚ_max : 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ₚ
-- 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 : 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
have refine : comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) Qₚ) = P
Tactic: refine ⟨comap (algebraMap S Sₚ) Qₚ, ⟨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 : 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ₚ)
⊢ comap (F := R →+* S) (algebraMap R S) (comap (F := S →+* Sₚ) (algebraMap S Sₚ) Qₚ) = P
have 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)))
Tactic: convert! Localization.AtPrime.under_maximalIdeal (I := P)
-- 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 : 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) (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)))
have 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) sorry)
      (algebraMap R Rₚ))
    Qₚ)
  (under R (comap (F := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) Qₚ))
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⟩)]