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
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)
rwa₁ rwa₂ rwa₃ 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) ⋯) :
          (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)

Tactic:
rwa [← RingHom.coe_comp, ← Localization.localRingHom_comp] at this

Premises used: RingHom.coe_comp, Localization.localRingHom_comp
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
hf : f.SurjectiveOnStalks
P : Ideal R
inst_2 : P.IsPrime
Q : Ideal S
inst_3 : Q.IsPrime
e : P = Ideal.comap f Q
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime P) (β := Localization.AtPrime Q)
    (⇑(Localization.localRingHom P Q f e) : (a : Localization.AtPrime P) → Localization.AtPrime Q)

Tactic:
e ▸ hf Q _

Premises used: Eq.symm
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
rw : 1 ∉ J
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := T) 1 1 ∉ J

Tactic:
rw [one_smul]

Premises used: one_smul
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
⊢ 1 ∉ J

Tactic:
J.primeCompl.one_mem

Premises used: Set.Mem, setOf, Submonoid.one_mem, Ideal.primeCompl, Not
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
⊢ 1 ∉ J

Tactic:
exact J.primeCompl.one_mem

Premises used: Submonoid.one_mem, Ideal.primeCompl
-- 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
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)
rw₁ rw₂ : Eq (α := S ⊗[R] T) 0 0
⊢ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := T) 1 1) 0 = 0 ⊗ₜ[R] 1

Tactic:
rw [mul_zero, TensorProduct.zero_tmul]

Premises used: TensorProduct.zero_tmul, MulZeroClass.mul_zero
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) 0 = a ⊗ₜ[R] t

Tactic:
exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem,
      by rw [mul_zero, TensorProduct.zero_tmul]⟩
-- 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
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
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
⊢ ∃ (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₂

Premises used: Iff.mp, RingHom.surjective_localRingHom_iff
-- 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
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)
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
⊢ ∃ (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:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
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

Tactic:
⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩

Premises used: Submonoid.mul_mem, And.intro, Exists.intro, HSMul.hSMul, Ideal.primeCompl
-- 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
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)
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
⊢ ∃ (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:
refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
-- 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
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)
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)
tmul₁ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) s : T) c * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₂ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] (HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) s : T) * x₂)) ((y • x₁) ⊗ₜ[R] c)
tmul₃ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) ((y • x₁) ⊗ₜ[R] c)
tmul₄ : Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T)) (x₁ ⊗ₜ[R] (y • c))
tmul₅ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (β := T) c ((algebraMap R T : (a : R) → T) y : T))
    (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
tmul₆ tmul₇ :
  Eq (α := S ⊗[R] T) (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
    (x₁ ⊗ₜ[R] HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) y : T) c)
⊢ 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:
rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.tmul_mul_tmul, mul_comm, Algebra.smul_def, one_mul
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
hx₁ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ = a ⊗ₜ[R] t
hx₂ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₂ = a ⊗ₜ[R] t
add :
  ∀ (t₁ : T) (r₁ : R) (a₁ : S) (hr₁ : r₁ • t₁ ∉ J) (e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁),
    ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t

Tactic:
obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
hx₂ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₂ = a ⊗ₜ[R] t
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
add :
  ∀ (t₂ : T) (r₂ : R) (a₂ : S) (hr₂ : r₂ • t₂ ∉ J) (e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂),
    ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t

Tactic:
obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
simp_rw : (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂
⊢ (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂

Tactic:
simp_rw [← smul_eq_mul]

Premises used: smul_eq_mul
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
rw rw₁ : (r₁ • t₁) • r₂ • t₂ = (r₁ • t₁) • r₂ • t₂
⊢ (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂

Tactic:
rw [smul_smul_smul_comm]

Premises used: smul_smul_smul_comm
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂

Tactic:
have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by
      simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t

Tactic:
⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩

Premises used: HMul.hMul, Submonoid.mul_mem, Eq.rec, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, Ideal.primeCompl, Eq.symm
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
this : (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
add : 1 ⊗ₜ[R] ((r₁ * r₂) • (t₁ * t₂)) * (x₁ + x₂) = (r₂ • a₁ + r₁ • a₂) ⊗ₜ[R] (t₁ * t₂)
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t

Tactic:
refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf₂ : SurjectiveOnStalks (algebraMap R T)
x : S ⊗[R] T
J : Ideal T
hJ : J.IsPrime
zero : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ HMul.hMul (α := S ⊗[R] T) (1 ⊗ₜ[R] (r • t)) 0 = a ⊗ₜ[R] t
tmul :
  ∀ (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
add :
  ∀ (x₁ x₂ : S ⊗[R] T) (hx₁ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ = a ⊗ₜ[R] t)
    (hx₂ : ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₂ = a ⊗ₜ[R] t),
    ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * (x₁ + x₂) = a ⊗ₜ[R] t
⊢ ∃ (t : T) (r : R) (a : S), r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t

Tactic:
induction x with
  | zero =>
    exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem,
      by rw [mul_zero, TensorProduct.zero_tmul]⟩
  | tmul x₁ x₂ =>
    obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂
    simp_rw [Algebra.smul_def]
    refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
    rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e,
      TensorProduct.smul_tmul, Algebra.smul_def, mul_comm]
  | add x₁ x₂ hx₁ hx₂ =>
    obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
    obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
    have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by
      simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
    refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
    rw [this, ← one_mul (1 : S), ← Algebra.TensorProduct.tmul_mul_tmul, mul_add, mul_comm (_ ⊗ₜ _),
      mul_assoc, e₁, Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc,
      ← TensorProduct.smul_tmul, mul_comm (_ ⊗ₜ _), mul_assoc, e₂,
      Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc, ← TensorProduct.smul_tmul,
      TensorProduct.add_tmul, mul_comm t₁ t₂]

Premises used: TensorProduct.smul_tmul, mul_assoc, smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul, mul_comm, TensorProduct.add_tmul, Algebra.smul_def, mul_add, TensorProduct.tmul, OfNat.ofNat, one_mul
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ SurjectiveOnStalks (algebraMap R S)

Tactic:
surjectiveOnStalks_of_exists_div fun s ↦ ?_

Premises used: RingHom.surjectiveOnStalks_of_exists_div
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
refine :
  ∀ (s : S),
    ∃ (r : R) (s_1 : R),
      IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) s_1 : S) ∧
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) s_1 : S) s = (algebraMap R S : (a : R) → S) r
⊢ SurjectiveOnStalks (algebraMap R S)

Tactic:
refine surjectiveOnStalks_of_exists_div fun s ↦ ?_

Premises used: RingHom.surjectiveOnStalks_of_exists_div
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
s : S
obtain :
  ∀ (x : R) (s : ↥M),
    ∃ (r : R) (s_1 : R),
      IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) s_1 : S) ∧
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) s_1 : S) (IsLocalization.mk' S x s) =
          (algebraMap R S : (a : R) → S) r
⊢ ∃ (r : R) (s_1 : R),
    IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) s_1 : S) ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) s_1 : S) s = (algebraMap R S : (a : R) → S) r

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M s

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
s : ↥M
⊢ ∃ (r : R) (s_1 : R),
    IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) s_1 : S) ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) s_1 : S) (IsLocalization.mk' S x s) =
        (algebraMap R S : (a : R) → S) r

Tactic:
⟨x, s, IsLocalization.map_units S s, IsLocalization.mk'_spec' S x s⟩

Premises used: IsLocalization.mk'_spec', And.intro, Exists.intro, IsLocalization.map_units, Subtype.val
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
s : ↥M
⊢ ∃ (r : R) (s_1 : R),
    IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) s_1 : S) ∧
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) s_1 : S) (IsLocalization.mk' S x s) =
        (algebraMap R S : (a : R) → S) r

Tactic:
exact ⟨x, s, IsLocalization.map_units S s, IsLocalization.mk'_spec' S x s⟩
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf : SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
rw :
  ∀ (s : S ⊗[R] T),
    ∃ (x : S) (r : S),
      ∃ c ∉ J,
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) ∉ J ∧
          HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) * s =
            HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x : S ⊗[R] T)
⊢ Function.Surjective (α := Localization.AtPrime (Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) J)) (β :=
    Localization.AtPrime J)
    (⇑(Localization.localRingHom (Ideal.comap (F := S →+* S ⊗[R] T) (algebraMap S (S ⊗[R] T)) J) J
          (algebraMap S (S ⊗[R] T)) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (algebraMap S (S ⊗[R] T)) J)) → Localization.AtPrime J)

Tactic:
rw [surjective_localRingHom_iff]

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
T : Type u_3
inst_2 : CommRing T
inst_3 : Algebra R T
inst_4 : Algebra R S
hf : SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
obtain :
  ∀ (t : T) (r : R) (a : S) (ht : r • t ∉ Ideal.comap g J) (e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t),
    ∃ (x_1 : S) (r : S),
      ∃ c ∉ J,
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) ∉ J ∧
          HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) * x =
            HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x_1 : S ⊗[R] T)
⊢ ∃ (x_1 : S) (r : S),
    ∃ c ∉ J,
      ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) ∉ J ∧
        HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) * x =
          HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x_1 : S ⊗[R] T)

Tactic:
obtain ⟨t, r, a, ht, e⟩ := hf.exists_mul_eq_tmul x (J.comap g) inferInstance

Premises used: RingHom.SurjectiveOnStalks.exists_mul_eq_tmul, inferInstance, Ideal.comap
-- 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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf : SurjectiveOnStalks (algebraMap R T)
g : T →+* S ⊗[R] T := AlgHom.toRingHom Algebra.TensorProduct.includeRight
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ ∃ (x_1 : S) (r : S),
    ∃ c ∉ J,
      ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) ∉ J ∧
        HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) * x =
          HMul.hMul (β := S ⊗[R] T) c ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x_1 : S ⊗[R] T)

Tactic:
⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩

Premises used: Algebra.algebraMap, And.intro, Exists.intro, HSMul.hSMul, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe