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
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 (α := ↥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)
have 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)
Tactic: simp only [Submonoid.coe_mul]
-- 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)
⊢ 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)
have 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)
Tactic: convert! congr($(ey.symm) * $(et)) using 1
-- 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)
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)
⊢ 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)
have 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)
Tactic: convert! congr($(ey.symm) * $(et)) using 1
-- 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
⊢ 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)
have 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)
Tactic: simp_rw [SurjectiveOnStalks, surjective_localRingHom_iff]
-- 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),
      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)
have 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)
Tactic: refine ⟨fun H I hI s ↦ ?_, fun H I hI ↦ H I hI.ne_top⟩
-- 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
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)
have 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)
Tactic: obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI
-- 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
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 : 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)
have 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)
Tactic: obtain ⟨x, r, c, hc, hr, e⟩ := H M hM.isPrime s
-- 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
⊢ 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)
have 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 sorry) :
          (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 sorry) :
      (a : Localization.AtPrime (Ideal.comap f I)) → Localization.AtPrime I)
Tactic: refine ⟨fun H I hI ↦ H I hI.isPrime, fun H I hI ↦ ?_⟩
-- 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
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)
have 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)
Tactic: simp_rw [surjective_localRingHom_iff] at H ⊢
Cleared hypotheses: H
-- 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
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI.ne_top
-- 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
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 : 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)
have 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)
Tactic: obtain ⟨x, r, c, hc, hr, e⟩ := H M hM s
-- 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
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 (g.comp f) I)) (β :=
    Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (g.comp f) I)) → Localization.AtPrime I)
have this : 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 sorry) :
      (a : Localization.AtPrime (Ideal.comap g I)) → Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f sorry) :
      (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))
-- 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
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
this :
  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)))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap (g.comp f) I)) (β :=
    Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (g.comp f) I)) → Localization.AtPrime I)
have rwa : ∀
  (this :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) (β :=
      Localization.AtPrime I)
      (⇑(RingHom.comp (β := Localization.AtPrime (Ideal.comap g I)) (Localization.localRingHom (Ideal.comap g I) I g sorry)
            (Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f sorry)) :
        (a : Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) → Localization.AtPrime I)),
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap (g.comp f) I)) (β :=
    Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) sorry) :
      (a : Localization.AtPrime (Ideal.comap (g.comp f) I)) → Localization.AtPrime I)
Tactic: rwa [← RingHom.coe_comp, ← Localization.localRingHom_comp] at this
Cleared hypotheses: this
-- 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
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
this :
  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)))
rwa :
  ∀
    (this :
      Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) (β :=
        Localization.AtPrime I)
        (⇑(RingHom.comp (β := Localization.AtPrime (Ideal.comap g I))
              (Localization.localRingHom (Ideal.comap g I) I g ⋯)
              (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 I)),
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap (g.comp f) I)) (β :=
      Localization.AtPrime I)
      (⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯) :
        (a : Localization.AtPrime (Ideal.comap (g.comp f) I)) → Localization.AtPrime I)
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap (g.comp f) I)) (β :=
    Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (g.comp f) I)) → Localization.AtPrime I)
have rwa₁ : ∀
  (this :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) (β :=
      Localization.AtPrime I)
      (⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) I (g.comp f) sorry) :
        (a : Localization.AtPrime (Ideal.comap f (Ideal.comap g I))) → Localization.AtPrime I)),
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := Localization.AtPrime (Ideal.comap (g.comp f) I)) (β :=
    Localization.AtPrime I)
    (⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) sorry) :
      (a : Localization.AtPrime (Ideal.comap (g.comp f) I)) → Localization.AtPrime I)
Tactic: rwa [← RingHom.coe_comp, ← Localization.localRingHom_comp] at this
Cleared hypotheses: this
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := T) 1 1 ∉ J
have rw : 1 ∉ J
Tactic: rw [one_smul]
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := T) 1 1) 0 = 0 ⊗ₜ[R] 1
have rw : Eq (α := S ⊗[R] T) 0 (0 ⊗ₜ[R] 1)
Tactic: rw [mul_zero, TensorProduct.zero_tmul]
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
rw : Eq (α := S ⊗[R] T) 0 (0 ⊗ₜ[R] 1)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := T) 1 1) 0 = 0 ⊗ₜ[R] 1
have rw₁ : Eq (α := S ⊗[R] T) 0 0
Tactic: rw [mul_zero, TensorProduct.zero_tmul]
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) (x₁ ⊗ₜ[R] x₂) = a ⊗ₜ[R] t
have tmul : ∀ (y s : R) (c : T) (hs : c ∉ J) (hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J)
  (e :
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
      HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)),
  ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) (x₁ ⊗ₜ[R] x₂) = a ⊗ₜ[R] t
Tactic: obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) (x₁ ⊗ₜ[R] x₂) = a ⊗ₜ[R] t
have tmul : ∃ (t : T) (r : R) (a : S),
  HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) t ∉ J ∧
    HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) t) (x₁ ⊗ₜ[R] x₂) =
      a ⊗ₜ[R] t
Tactic: simp_rw [Algebra.smul_def]
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
⊢ ∃ (t : T) (r : R) (a : S),
    HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) t ∉ J ∧
      HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) t) (x₁ ⊗ₜ[R] x₂) =
        a ⊗ₜ[R] t
have tmul : HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
  (y • x₁) ⊗ₜ[R] c
Tactic: refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
-- 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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : ((algebraMap R T : (a : R) → T) s : T) ∉ J
e :
  HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂ =
    HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c) (x₁ ⊗ₜ[R] x₂) =
    (y • x₁) ⊗ₜ[R] c
have tmul : Eq (α := S ⊗[R] T) ((1 * x₁) ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂))
  ((y • x₁) ⊗ₜ[R] c)
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]