awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
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)) ⋯) : 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)
⊢ ∃ (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
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
⊢ 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

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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) =
    HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) (↑t : R) : 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:
⟨_, _, _, c.2, t.2, hc.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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) =
    HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) (↑t : R) : 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:
exact ⟨_, _, _, c.2, t.2, hc.symm⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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)

Tactic:
fun H y ↦ Localization.ind (fun ⟨y, t, h⟩ ↦ ?_) y

Premises used: Localization.ind, Function.Surjective
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
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 ⋯ :
                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)
⊢ (∀ (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)

Tactic:
refine fun H y ↦ Localization.ind (fun ⟨y, t, h⟩ ↦ ?_) y
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
mpr :
  ∃ (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)
⊢ ∃ (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)

Tactic:
simp only
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
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 ⋯ :
                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)
⊢ ∃ (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)

Tactic:
obtain ⟨yx, ys, yc, hyc, hy, ey⟩ := H y
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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)
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 ⋯ :
                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)
⊢ ∃ (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)

Tactic:
obtain ⟨tx, ts, yt, hyt, ht, et⟩ := H t
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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)

Tactic:
⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩

Premises used: Localization.mk, HMul.hMul, Submonoid.mul_mem, Subtype.mk, Exists.intro
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
mpr₁ :
  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)
⊢ ∃ (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)

Tactic:
refine ⟨Localization.mk (yx * ts) ⟨ys * tx, Submonoid.mul_mem _ hy ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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)
⊢ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap f P)) tx

Tactic:
fun H ↦ mul_mem (P.primeCompl.mul_mem hyt ht) h (et ▸ Ideal.mul_mem_left _ yt H)

Premises used: Submonoid.mul_mem, Set.Mem, setOf, Eq.rec, Ideal.primeCompl, Ideal.mul_mem_left, Eq.symm, Not, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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)
⊢ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap f P)) tx

Tactic:
exact fun H ↦ mul_mem (P.primeCompl.mul_mem hyt ht) h (et ▸ Ideal.mul_mem_left _ yt H)

Premises used: Submonoid.mul_mem, Ideal.primeCompl, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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 :
  ∃ (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)
⊢ 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)

Tactic:
simp only [Localization.mk_eq_mk', Localization.localRingHom_mk', map_mul f,
        IsLocalization.mk'_eq_iff_eq, IsLocalization.eq_iff_exists P.primeCompl]

Premises used: Localization.mk_eq_mk', Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, map_mul, Ideal.primeCompl, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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)

Tactic:
⟨⟨yc, hyc⟩ * ⟨yt, hyt⟩, ?_⟩

Premises used: HMul.hMul, Exists.intro
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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 :
  (↑(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)
⊢ ∃ (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:
refine ⟨⟨yc, hyc⟩ * ⟨yt, hyt⟩, ?_⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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 :
  yc * yt * (t * HMul.hMul (α := S) (β := S) ((f : (a : R) → S) yx : S) ((f : (a : R) → S) ts : S)) =
    yc * yt * (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ys : S) ((f : (a : R) → S) tx : S) * y)
⊢ (↑(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:
simp only [Submonoid.coe_mul]

Premises used: Submonoid.coe_mul