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 :
  ∀ (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)
⊢ HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S) * (HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t) =
    HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y * HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)

Tactic:
congr($(ey.symm) * $(et))

Premises used: HMul.hMul, congrArg, id, congr, Eq.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
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)
h₁ :
  yc * yt * (t * HMul.hMul (α := S) (β := S) ((f : (a : R) → S) yx : S) ((f : (a : R) → S) ts : S)) =
    HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S) * (HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t)
h₂ :
  yc * yt * (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ys : S) ((f : (a : R) → S) tx : S) * y) =
    HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y * HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)
⊢ 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)

Tactic:
convert! congr($(ey.symm) * $(et)) using 1

Premises used: Eq.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
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)
⊢ yc * yt * (t * HMul.hMul (α := S) (β := S) ((f : (a : R) → S) yx : S) ((f : (a : R) → S) ts : S)) =
    HMul.hMul (β := S) yc ((f : (a : R) → S) yx : S) * (HMul.hMul (β := S) yt ((f : (a : R) → S) ts : S) * t)

Tactic:
ring
-- 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)
⊢ yc * yt * (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) ys : S) ((f : (a : R) → S) tx : S) * y) =
    HMul.hMul (β := S) yc ((f : (a : R) → S) ys : S) * y * HMul.hMul (β := S) yt ((f : (a : R) → S) tx : S)

Tactic:
ring
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
simp_rw :
  (∀ (P : Ideal S),
      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)) ↔
    ∀ (I : Ideal S),
      I ≠ ⊤ →
        ∀ (s : S),
          ∃ (x : R) (r : R),
            ∃ c ∉ I,
              ((f : (a : R) → S) r : S) ∉ I ∧
                HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S),
      I ≠ ⊤ →
        ∀ (s : S),
          ∃ (x : R) (r : R),
            ∃ c ∉ I,
              ((f : (a : R) → S) r : S) ∉ I ∧
                HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
simp_rw [SurjectiveOnStalks, surjective_localRingHom_iff]

Premises used: RingHom.SurjectiveOnStalks, RingHom.surjective_localRingHom_iff
-- 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),
      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)) ↔
    ∀ (I : Ideal S),
      I ≠ ⊤ →
        ∀ (s : S),
          ∃ (x : R) (r : R),
            ∃ c ∉ I,
              ((f : (a : R) → S) r : S) ∉ I ∧
                HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
⟨fun H I hI s ↦ ?_, fun H I hI ↦ H I hI.ne_top⟩

Premises used: Iff.intro, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
refine :
  ∀
    (H :
      ∀ (P : Ideal S),
        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))
    (I : Ideal S) (hI : I ≠ ⊤) (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ I,
        ((f : (a : R) → S) r : S) ∉ I ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ (∀ (P : Ideal S),
      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)) ↔
    ∀ (I : Ideal S),
      I ≠ ⊤ →
        ∀ (s : S),
          ∃ (x : R) (r : R),
            ∃ c ∉ I,
              ((f : (a : R) → S) r : S) ∉ I ∧
                HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
refine ⟨fun H I hI s ↦ ?_, fun H I hI ↦ H I hI.ne_top⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (P : Ideal S),
    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)
I : Ideal S
hI : I ≠ ⊤
s : S
obtain :
  ∀ (M : Ideal S) (hM : M.IsMaximal) (hIM : I ≤ M),
    ∃ (x : R) (r : R),
      ∃ c ∉ I,
        ((f : (a : R) → S) r : S) ∉ I ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (P : Ideal S),
    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)
I : Ideal S
hI : I ≠ ⊤
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
obtain :
  ∀ (x r : R) (c : S) (hc : c ∉ M) (hr : ((f : (a : R) → S) r : S) ∉ M)
    (e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)),
    ∃ (x : R) (r : R),
      ∃ c ∉ I,
        ((f : (a : R) → S) r : S) ∉ I ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
obtain ⟨x, r, c, hc, hr, e⟩ := H M hM.isPrime s

Premises used: Ideal.IsMaximal.isPrime
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (P : Ideal S),
    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)
I : Ideal S
hI : I ≠ ⊤
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
x r : R
c : S
hc : c ∉ M
hr : ((f : (a : R) → S) r : S) ∉ M
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩

Premises used: And.intro, 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
H :
  ∀ (P : Ideal S),
    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)
I : Ideal S
hI : I ≠ ⊤
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
x r : R
c : S
hc : c ∉ M
hr : ((f : (a : R) → S) r : S) ∉ M
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
exact ⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S) (x : I.IsMaximal),
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f I)) (β := Localization.AtPrime I)
        (⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯) :
          (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I)

Tactic:
⟨fun H I hI ↦ H I hI.isPrime, fun H I hI ↦ ?_⟩

Premises used: Ideal.IsMaximal.isPrime, Iff.intro
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
refine :
  ∀
    (H :
      ∀ (I : Ideal S) (x : I.IsMaximal),
        Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f I)) (β :=
          Localization.AtPrime I)
          (⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯) :
            (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I))
    (I : Ideal S) (hI : I.IsPrime),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f I)) (β := Localization.AtPrime I)
      (⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I)
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S) (x : I.IsMaximal),
      Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f I)) (β := Localization.AtPrime I)
        (⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯) :
          (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I)

Tactic:
refine ⟨fun H I hI ↦ H I hI.isPrime, fun H I hI ↦ ?_⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (I : Ideal S) (x : I.IsMaximal),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f I)) (β := Localization.AtPrime I)
      (⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I)
I : Ideal S
hI : I.IsPrime
simp_rw :
  ∀
    (H :
      ∀ (I : Ideal S),
        I.IsMaximal →
          ∀ (s : S),
            ∃ (x : R) (r : R),
              ∃ c ∉ I,
                ((f : (a : R) → S) r : S) ∉ I ∧
                  HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S))
    (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ I,
        ((f : (a : R) → S) r : S) ∉ I ∧
          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 I)) (β := Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I)

Tactic:
simp_rw [surjective_localRingHom_iff] at H ⊢

Premises used: RingHom.surjective_localRingHom_iff
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hI : I.IsPrime
H :
  ∀ (I : Ideal S),
    I.IsMaximal →
      ∀ (s : S),
        ∃ (x : R) (r : R),
          ∃ c ∉ I,
            ((f : (a : R) → S) r : S) ∉ I ∧
              HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
s : S
obtain :
  ∀ (M : Ideal S) (hM : M.IsMaximal) (hIM : I ≤ M),
    ∃ (x : R) (r : R),
      ∃ c ∉ I,
        ((f : (a : R) → S) r : S) ∉ I ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI.ne_top

Premises used: Ideal.exists_le_maximal, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hI : I.IsPrime
H :
  ∀ (I : Ideal S),
    I.IsMaximal →
      ∀ (s : S),
        ∃ (x : R) (r : R),
          ∃ c ∉ I,
            ((f : (a : R) → S) r : S) ∉ I ∧
              HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
obtain :
  ∀ (x r : R) (c : S) (hc : c ∉ M) (hr : ((f : (a : R) → S) r : S) ∉ M)
    (e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)),
    ∃ (x : R) (r : R),
      ∃ c ∉ I,
        ((f : (a : R) → S) r : S) ∉ I ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
obtain ⟨x, r, c, hc, hr, e⟩ := H M hM s
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
I : Ideal S
hI : I.IsPrime
H :
  ∀ (I : Ideal S),
    I.IsMaximal →
      ∀ (s : S),
        ∃ (x : R) (r : R),
          ∃ c ∉ I,
            ((f : (a : R) → S) r : S) ∉ I ∧
              HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
x r : R
c : S
hc : c ∉ M
hr : ((f : (a : R) → S) r : S) ∉ M
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩

Premises used: And.intro, 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
I : Ideal S
hI : I.IsPrime
H :
  ∀ (I : Ideal S),
    I.IsMaximal →
      ∀ (s : S),
        ∃ (x : R) (r : R),
          ∃ c ∉ I,
            ((f : (a : R) → S) r : S) ∉ I ∧
              HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
s : S
M : Ideal S
hM : M.IsMaximal
hIM : I ≤ M
x r : R
c : S
hc : c ∉ M
hr : ((f : (a : R) → S) r : S) ∉ M
e : HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ I,
      ((f : (a : R) → S) r : S) ∉ I ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
exact ⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔
    ∀ (I : Ideal S),
      I.IsMaximal →
        ∀ (s : S),
          ∃ (x : R) (r : R),
            ∃ c ∉ I,
              ((f : (a : R) → S) r : S) ∉ I ∧
                HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
simp only [surjectiveOnStalks_iff_forall_maximal, surjective_localRingHom_iff]

Premises used: RingHom.surjectiveOnStalks_iff_forall_maximal, RingHom.surjective_localRingHom_iff
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (x : S),
    ∃ (r : R) (s : R),
      IsUnit.{u_2} (M := S) ((f : (a : R) → S) s : S) ∧
        HMul.hMul (α := S) ((f : (a : R) → S) s : S) x = (f : (a : R) → S) r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) s : S)
hr' : HMul.hMul (α := S) ((f : (a : R) → S) s : S) x = (f : (a : R) → S) r
⊢ 1 ∉ I

Tactic:
simpa [← Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (x : S),
    ∃ (r : R) (s : R),
      IsUnit.{u_2} (M := S) ((f : (a : R) → S) s : S) ∧
        HMul.hMul (α := S) ((f : (a : R) → S) s : S) x = (f : (a : R) → S) r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit.{u_2} (M := S) ((f : (a : R) → S) s : S)
hr' : HMul.hMul (α := S) ((f : (a : R) → S) s : S) x = (f : (a : R) → S) r
⊢ HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) s : S) * x =
    HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) r : S)

Tactic:
simpa
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : Ideal S
h_1 : x ≠ ⊤
s : S
r : R
hr : (f : (a : R) → S) r = s
⊢ 1 ∉ x

Tactic:
simpa [← Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : Ideal S
h_1 : x ≠ ⊤
s : S
r : R
hr : (f : (a : R) → S) r = s
⊢ ((f : (a : R) → S) 1 : S) ∉ x

Tactic:
simpa [← Ideal.eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
h : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : Ideal S
h_1 : x ≠ ⊤
s : S
r : R
hr : (f : (a : R) → S) r = s
⊢ HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) 1 : S) * s =
    HMul.hMul (α := S) (β := S) (1 : S) ((f : (a : R) → S) r : S)

Tactic:
simp [hr]
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.SurjectiveOnStalks

Tactic:
RingHom.surjectiveOnStalks_of_surjective e.surjective

Premises used: RingEquiv.surjective, RingHom.surjectiveOnStalks_of_surjective
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : g.SurjectiveOnStalks
hf : f.SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) (β :=
    Localization.AtPrime I)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := Localization.AtPrime (Ideal.comap g I))
      (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) :
        (a : Localization.AtPrime (Ideal.comap g I)) → Localization.AtPrime I)
      (⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) → Localization.AtPrime (Ideal.comap g I)))

Tactic:
have := (hg I hI).comp (hf _ (hI.comap g))