awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
mp :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
      (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P) →
    ∀ (s : S),
      ∃ (x : R) (r : R),
        ∃ c ∉ P,
          ((f : (a : R) → S) r : S) ∉ P ∧
            HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
      (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P) ↔
    ∀ (s : S),
      ∃ (x : R) (r : R),
        ∃ c ∉ P,
          ((f : (a : R) → S) r : S) ∉ P ∧
            HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have mpr : (∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)) →
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f sorry) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
y : S
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have mp : ∀ (a : Localization.AtPrime (Ideal.comap f P))
  (ha :
    Eq (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f sorry :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)),
  ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
Tactic: obtain ⟨a, ha⟩ := H (IsLocalization.mk' _ y (1 : P.primeCompl))
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
y : S
a : Localization.AtPrime (Ideal.comap f P)
ha :
  Eq (α := Localization.AtPrime P)
    (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
          (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
        a :
      Localization.AtPrime P)
    (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have mp : ∀ (a : R) (t : ↥(Ideal.primeCompl (Ideal.comap f P)))
  (ha :
    Eq (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f sorry :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) :
        Localization.AtPrime P)
      (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)),
  ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
Tactic: obtain ⟨a, t, rfl⟩ := IsLocalization.exists_mk'_eq (P.comap f).primeCompl a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
y : S
a : R
t : ↥(Ideal.primeCompl (Ideal.comap f P))
ha :
  Eq (α := Localization.AtPrime P)
    (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
          (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
        (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) :
      Localization.AtPrime P)
    (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have ha₁ : ∃ (c : ↥P.primeCompl),
  HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) a : S) =
    (↑c : S) *
      HMul.hMul (α := S) ((↑(Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) ((f : (a : R) → S) (↑t : R)) sorry) : S) : S)
        y
Tactic: rw [Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq,
      Submonoid.coe_one, one_mul, IsLocalization.eq_iff_exists P.primeCompl] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
y : S
a : R
t : ↥(Ideal.primeCompl (Ideal.comap f P))
ha :
  ∃ (c : ↥P.primeCompl),
    HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) a : S) =
      (↑c : S) *
        HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) ((f : (a : R) → S) (↑t : R)) ⋯) : S) : S) y
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have mp : ∀ (c : ↥P.primeCompl)
  (hc :
    HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) a : S) =
      (↑c : S) *
        HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) ((f : (a : R) → S) (↑t : R)) sorry) : S) : S) y),
  ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
Tactic: obtain ⟨c, hc⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
y : S
a : R
t : ↥(Ideal.primeCompl (Ideal.comap f P))
c : ↥P.primeCompl
hc :
  HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) a : S) =
    (↑c : S) *
      HMul.hMul (α := S) ((↑(Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) ((f : (a : R) → S) (↑t : R)) ⋯) : S) : S)
        y
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have hc₁ : HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) a : S) = HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) (↑t : R) : S) * y
Tactic: simp only [← mul_assoc] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
⊢ (∀ (s : S),
      ∃ (x : R) (r : R),
        ∃ c ∉ P,
          ((f : (a : R) → S) r : S) ∉ P ∧
            HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)) →
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
      (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
have mpr : ∀
  (H :
    ∀ (s : S),
      ∃ (x : R) (r : R),
        ∃ c ∉ P,
          ((f : (a : R) → S) r : S) ∉ P ∧
            HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S))
  (y : Localization.AtPrime P) (x : S × ↥P.primeCompl) (y t : S) (h : t ∈ P.primeCompl),
  ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f sorry :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk (y, Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h).1
          (y, Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h).2 :
        Localization (M := S) P.primeCompl)
Tactic: refine fun H y ↦ Localization.ind (fun ⟨y, t, h⟩ ↦ ?_) y
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk (y, Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h).1
          (y, Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h).2 :
        Localization (M := S) P.primeCompl)
have mpr : ∃ (a : Localization.AtPrime (Ideal.comap f P)),
  Eq.{u_2 + 1} (α := Localization.AtPrime P)
    (((Localization.localRingHom (Ideal.comap f P) P f sorry :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
          (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
        a :
      Localization.AtPrime P)
    (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
⊢ ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
have mpr : ∀ (yx ys : R) (yc : S) (hyc : yc ∉ P) (hy : ((f : (a : R) → S) ys : S) ∉ P)
  (ey : HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y = HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S)),
  ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f sorry :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
Tactic: obtain ⟨yx, ys, yc, hyc, hy, ey⟩ := H y
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : ((f : (a : R) → S) ys : S) ∉ P
ey : HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y = HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S)
⊢ ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
have mpr : ∀ (tx ts : R) (yt : S) (hyt : yt ∉ P) (ht : ((f : (a : R) → S) ts : S) ∉ P)
  (et : HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t = HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)),
  ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f sorry :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
Tactic: obtain ⟨tx, ts, yt, hyt, ht, et⟩ := H t
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : ((f : (a : R) → S) ys : S) ∉ P
ey : HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y = HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S)
tx ts : R
yt : S
hyt : yt ∉ P
ht : ((f : (a : R) → S) ts : S) ∉ P
et : HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t = HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)
⊢ ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
have mpr : Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap f P)) tx
Tactic: refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : ((f : (a : R) → S) ys : S) ∉ P
ey : HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y = HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S)
tx ts : R
yt : S
hyt : yt ∉ P
ht : ((f : (a : R) → S) ts : S) ∉ P
et : HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t = HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)
mpr : Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap f P)) tx
⊢ ∃ (a : Localization.AtPrime (Ideal.comap f P)),
    Eq.{u_2 + 1} (α := Localization.AtPrime P)
      (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
              RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
            (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
          a :
        Localization.AtPrime P)
      (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
have mpr₁ : Eq.{u_2 + 1} (α := Localization.AtPrime P)
  (((Localization.localRingHom (Ideal.comap f P) P f sorry :
          RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
        (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
      (Localization.mk (yx * ts)
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap f P)) x)
          (ys * tx) sorry)) :
    Localization.AtPrime P)
  (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
Tactic: refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : ((f : (a : R) → S) ys : S) ∉ P
ey : HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y = HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S)
tx ts : R
yt : S
hyt : yt ∉ P
ht : ((f : (a : R) → S) ts : S) ∉ P
et : HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t = HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime P)
    (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
          (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
        (Localization.mk (yx * ts)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap f P)) x)
            (ys * tx) ⋯)) :
      Localization.AtPrime P)
    (Localization.mk y (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) t h) : Localization (M := S) P.primeCompl)
have mpr : ∃ (c : ↥P.primeCompl),
  (↑c : S) * (t * HMul.hMul (α := S) (β := S) ((f : (a : R) → S) yx : S) ((f : (a : R) → S) ts : S)) =
    (↑c : S) * (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ys : S) ((f : (a : R) → S) tx : S) * y)
Tactic: simp only [Localization.mk_eq_mk', Localization.localRingHom_mk', map_mul f,
        IsLocalization.mk'_eq_iff_eq, IsLocalization.eq_iff_exists P.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
H :
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
y_1 : Localization.AtPrime P
x : S × ↥P.primeCompl
y t : S
h : t ∈ P.primeCompl
yx ys : R
yc : S
hyc : yc ∉ P
hy : ((f : (a : R) → S) ys : S) ∉ P
ey : HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y = HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S)
tx ts : R
yt : S
hyt : yt ∉ P
ht : ((f : (a : R) → S) ts : S) ∉ P
et : HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t = HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)
⊢ ∃ (c : ↥P.primeCompl),
    (↑c : S) * (t * HMul.hMul (α := S) (β := S) ((f : (a : R) → S) yx : S) ((f : (a : R) → S) ts : S)) =
      (↑c : S) * (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ys : S) ((f : (a : R) → S) tx : S) * y)
have mpr : (↑(HMul.hMul (α := ↥P.primeCompl) (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) yc hyc)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) yt hyt)) :
      S) *
    (t * HMul.hMul (α := S) (β := S) ((f : (a : R) → S) yx : S) ((f : (a : R) → S) ts : S)) =
  (↑(HMul.hMul (α := ↥P.primeCompl) (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) yc hyc)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) yt hyt)) :
      S) *
    (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ys : S) ((f : (a : R) → S) tx : S) * y)
Tactic: refine ⟨⟨yc, hyc⟩ * ⟨yt, hyt⟩, ?_⟩