awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
⊢ False
have rcases : ∀ (rz : R) (sz : ↥P.primeCompl) (hrz : mk' S rz sz = z), False
Tactic: rcases exists_mk'_eq P.primeCompl z with ⟨rz, sz, hrz⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hrz : mk' S rz sz = z
⊢ False
have rw : ∀ (hrx : mk' S rx sx = x) (ry : R) (sy : ↥P.primeCompl) (hry : mk' S ry sy = y) (rz : R) (sz : ↥P.primeCompl)
  (hxyz :
    mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
      mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 sorry))
  (hrz : mk' S rz sz = z), False
Tactic: rw [← hrx, ← hry, ← hrz, ← mk'_add, ← mk'_mul, ← mk'_self S P.primeCompl.one_mem] at hxyz
Cleared hypotheses: hxyz, hrx, ry, sy, hry, rz, sz, hrz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
⊢ False
have rw : ∀ (hx : mk' S rx sx ∈ nonunits S) (hrx : mk' S rx sx = x) (ry : R) (sy : ↥P.primeCompl) (hry : mk' S ry sy = y) (rz : R)
  (sz : ↥P.primeCompl)
  (hxyz :
    mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
      mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 sorry))
  (hrz : mk' S rz sz = z), False
Tactic: rw [← hrx] at hx
Cleared hypotheses: hx, hrx, ry, sy, hry, rz, sz, hxyz, hrz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
⊢ False
have rw : ∀ (hy : mk' S ry sy ∈ nonunits S) (hry : mk' S ry sy = y) (rz : R) (sz : ↥P.primeCompl)
  (hxyz :
    mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
      mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 sorry))
  (hrz : mk' S rz sz = z), False
Tactic: rw [← hry] at hy
Cleared hypotheses: hy, hry, rz, sz, hxyz, hrz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
⊢ False
have obtain : ∀ (t : ↥P.primeCompl)
  (ht :
    (↑t : R) *
        ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 sorry) : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz)) =
      (↑t : R) * ((↑(sx * sy * sz) : R) * 1)),
  False
Tactic: obtain ⟨t, ht⟩ := IsLocalization.eq.1 hxyz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht :
  (↑t : R) *
      ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯) : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz)) =
    (↑t : R) * ((↑(sx * sy * sz) : R) * 1)
⊢ False
have ht₁ : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
Tactic: simp only [mul_one, one_mul, Submonoid.coe_mul] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
⊢ False
have suffices : (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R)) ∈ P
Tactic: suffices (t : R) * (sx * sy * sz) ∈ P from
        not_or_intro (mt hp.mem_or_mem <| not_or_intro sx.2 sy.2) sz.2
          (hp.mem_or_mem <| (hp.mem_or_mem this).resolve_left t.2)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hu : IsUnit (x + y)
z : S
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hx : mk' S rx sx ∈ nonunits S
hrx : mk' S rx sx = x
ry : R
sy : ↥P.primeCompl
hy : mk' S ry sy ∈ nonunits S
hry : mk' S ry sy = y
rz : R
sz : ↥P.primeCompl
hxyz :
  mk' S ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) (sx * sy * sz) =
    mk' S 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ P.primeCompl) 1 ⋯)
hrz : mk' S rz sz = z
t : ↥P.primeCompl
ht : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) = (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R))
⊢ (↑t : R) * ((↑sx : R) * (↑sy : R) * (↑sz : R)) ∈ P
have rw : (↑t : R) * ((rx * (↑sy : R) + ry * (↑sx : R)) * rz) ∈ P
Tactic: rw [← ht]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_4 : IsLocalization.AtPrime S P
⊢ FaithfulSMul R S
have rw : ∀ (c : ↥P.primeCompl), IsRegular (↑c : R)
Tactic: rw [faithfulSMul_iff_algebraMap_injective, IsLocalization.injective_iff_isRegular P.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
A : Type u_4
inst_4 : CommRing A
inst_5 : IsDomain A
I : Ideal R
hI : I.IsPrime
inst_6 : IsLocalization.AtPrime S I
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ Disjoint (↑I.primeCompl : Set R) (↑p : Set R)}
    {p : Ideal R | p.IsPrime ∧ p ≤ I}
have h : ∀ (x : Ideal R),
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ Disjoint (↑I.primeCompl : Set R) (↑p : Set R)} x ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | p.IsPrime ∧ p ≤ I} x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Eq (α := Ideal (Localization.AtPrime I))
    (Ideal.map (F := R →+* Localization.AtPrime I) (algebraMap R (Localization.AtPrime I)) I)
    (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))
have h : Eq (α := Ideal (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))
  (Ideal.map (F := R →+* Localization.AtPrime I) (algebraMap R (Localization.AtPrime I))
    (Ideal.under R (B := Localization (M := R) I.primeCompl)
      (IsLocalRing.maximalIdeal (Localization (M := R) I.primeCompl))))
Tactic: convert! congr_arg (Ideal.map _) AtPrime.under_maximalIdeal.symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : Membership.mem (γ := Submodule R R) (Ideal.comap f J) x
⊢ x ∈ I
have contrapose : ∀ (hx : x ∉ I), x ∉ Ideal.comap f J
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_2 : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ Eq.{u_3 + 1} (α := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk x y) :
      Localization.AtPrime J)
    (mk ((f : (a : R) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑y : R)) ⋯) :
      Localization (M := P) J.primeCompl)
have simp_rw : Eq.{u_3 + 1} (α := Localization.AtPrime J)
  (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
        (a : Localization.AtPrime I) → Localization.AtPrime J)
      (mk' (Localization (M := R) I.primeCompl) x y) :
    Localization.AtPrime J)
  (mk' (R := P) (M := J.primeCompl) (Localization (M := P) J.primeCompl) ((f : (a : R) → P) x : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑y : R)) sorry : ↥J.primeCompl) :
    Localization (M := P) J.primeCompl)
Tactic: simp_rw [mk_eq_mk', localRingHom_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
hx :
  IsUnit.{u_3} (M := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        x :
      Localization.AtPrime J)
⊢ IsUnit x
have rcases : ∀ (r : R) (s : ↥I.primeCompl)
  (hx :
    IsUnit.{u_3} (M := Localization.AtPrime J)
      (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
            (a : Localization.AtPrime I) → Localization.AtPrime J)
          (mk' (Localization.AtPrime I) r s) :
        Localization.AtPrime J)),
  IsUnit (M := Localization.AtPrime I) (mk' (Localization.AtPrime I) r s)
Tactic: rcases IsLocalization.exists_mk'_eq I.primeCompl x with ⟨r, s, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx :
  IsUnit.{u_3} (M := Localization.AtPrime J)
    (((localRingHom I J f hIJ : RingHom.{u_1, u_3} (Localization.AtPrime I) (Localization.AtPrime J)) :
          (a : Localization.AtPrime I) → Localization.AtPrime J)
        (mk' (Localization.AtPrime I) r s) :
      Localization.AtPrime J)
⊢ IsUnit (M := Localization.AtPrime I) (mk' (Localization.AtPrime I) r s)
have hx₁ : IsUnit.{u_3} (M := Localization.AtPrime J)
  (mk' (R := P) (M := J.primeCompl) (Localization.AtPrime J) ((f : (a : R) → P) r : P)
    (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑s : R)) sorry : ↥J.primeCompl))
Tactic: rw [localRingHom_mk'] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx :
  IsUnit.{u_3} (M := Localization.AtPrime J)
    (mk' (R := P) (M := J.primeCompl) (Localization.AtPrime J) ((f : (a : R) → P) r : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ J.primeCompl) ((f : (a : R) → P) (↑s : R)) ⋯ : ↥J.primeCompl))
⊢ IsUnit (M := Localization.AtPrime I) (mk' (Localization.AtPrime I) r s)
have rw : ∀ (hx : Membership.mem (α := P) J.primeCompl ((f : (a : R) → P) r : P)), r ∈ I.primeCompl
Tactic: rw [AtPrime.isUnit_mk'_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst_4 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ I = Ideal.comap (g.comp f) K
have rw : Eq (α := Ideal R) (Ideal.comap f J) (Ideal.comap (g.comp f) K)
Tactic: rw [hIJ, hJK, Ideal.comap_comap f g]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst_4 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
rw : Eq (α := Ideal R) (Ideal.comap f J) (Ideal.comap (g.comp f) K)
⊢ I = Ideal.comap (g.comp f) K
have rw₁ : Eq (α := Ideal R) (Ideal.comap f (Ideal.comap g K)) (Ideal.comap (g.comp f) K)
Tactic: rw [hIJ, hJK, Ideal.comap_comap f g]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R S_1
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst_4 : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
rw : Eq (α := Ideal R) (Ideal.comap f J) (Ideal.comap (g.comp f) K)
rw₁ : Eq (α := Ideal R) (Ideal.comap f (Ideal.comap g K)) (Ideal.comap (g.comp f) K)
⊢ I = Ideal.comap (g.comp f) K
have rw₂ : Eq (α := Ideal R) (Ideal.comap (g.comp f) K) (Ideal.comap (g.comp f) K)
Tactic: rw [hIJ, hJK, Ideal.comap_comap f g]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) I
have rw : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap f J)
Tactic: rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
rw : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap f J)
⊢ J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) I
have rw₁ : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap (F := R →+* P) (↑f : R →+* P) J)
Tactic: rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
rw : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap f J)
rw₁ : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap (F := R →+* P) (↑f : R →+* P) J)
⊢ J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) I
have rw₂ : J =
  Ideal.comap (F := P →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* P) (↑f.symm : P →+* R)) J
Tactic: rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
rw : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap f J)
rw₁ : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap (F := R →+* P) (↑f : R →+* P) J)
rw₂ :
  J =
    Ideal.comap (F := P →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* P) (↑f.symm : P →+* R))
      J
⊢ J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) I
have rw₃ : J = Ideal.comap (F := P →+* P) (RingHom.id P) J
Tactic: rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst_4 : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
rw : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap f J)
rw₁ : J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) (Ideal.comap (F := R →+* P) (↑f : R →+* P) J)
rw₂ :
  J =
    Ideal.comap (F := P →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* P) (↑f.symm : P →+* R))
      J
rw₃ : J = Ideal.comap (F := P →+* P) (RingHom.id P) J
⊢ J = Ideal.comap (F := P →+* R) (↑f.symm : P →+* R) I
have rw₄ : J = J
Tactic: rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
have left : Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
  (⇑(localRingHom p P (algebraMap (↥s) S) sorry) : (a : Localization.AtPrime p) → Localization.AtPrime P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
left :
  Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
have right : Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
  (⇑(localRingHom p P (algebraMap (↥s) S) sorry) : (a : Localization.AtPrime p) → Localization.AtPrime P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
⊢ Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
have left : ∀ a ∈ s,
  ∀ b ∈ s,
    b ∉ P →
      ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Tactic: suffices ∀ a ∈ s, ∀ b ∈ s, b ∉ P → ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P,
        x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b) by
      simpa [Function.Injective, (IsLocalization.mk'_surjective p.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq', Subtype.ext_iff, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, IsLocalization.eq_iff_exists p.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal S
inst_3 : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
h : a ∈ s
b : S
h_1 : b ∈ s
h_2 : b ∉ P
c : S
h_3 : c ∈ s
d : S
h_4 : d ∈ s
h_5 : d ∉ P
x : S
hxP : x ∉ P
e : x * (a * d) = x * (c * b)
⊢ ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
have left : ∀ (t : S) (ht : t * x ∈ s) (htP : t ∈ (↑P.primeCompl : Set S)), ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Tactic: obtain ⟨t, ⟨htP, -⟩, ht⟩ := H.ge (Set.mem_univ x)