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
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
refine_1 : ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) ((algebraMap R S : (a : R) → S) r) : S ⊗[R] T) ∉ J
refine_2 :
  HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) (1 ⊗ₜ[R] (r • t))
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) ((algebraMap R S : (a : R) → S) r) : S ⊗[R] T) *
      x =
    HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) (1 ⊗ₜ[R] (r • t))
      ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : 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:
refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩
-- 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
H :
  Membership.mem (α := S ⊗[R] T) J
    ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) ((algebraMap R S : (a : R) → S) r) : S ⊗[R] T)
⊢ Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one (A := S), Algebra.TensorProduct.algebraMap_apply,
      Algebra.algebraMap_self, id_apply, smul_tmul, ← Algebra.algebraMap_eq_smul_one (A := T)] at H

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, Algebra.algebraMap_eq_smul_one
-- 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
H : Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
⊢ HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) ((g : (a : T) → S ⊗[R] T) ((algebraMap R T : (a : R) → T) r) : S ⊗[R] T)
      ((g : (a : T) → S ⊗[R] T) t : S ⊗[R] T) ∉
    J

Tactic:
rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht

Premises used: Algebra.smul_def, RingHom.map_mul, Ideal.mem_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
H : Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
ht₁ :
  HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) ((g : (a : T) → S ⊗[R] T) ((algebraMap R T : (a : R) → T) r) : S ⊗[R] T)
      ((g : (a : T) → S ⊗[R] T) t : S ⊗[R] T) ∉
    J
⊢ 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t

Tactic:
rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht

Premises used: Algebra.smul_def, RingHom.map_mul, Ideal.mem_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
H : Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
ht₁ :
  HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) ((g : (a : T) → S ⊗[R] T) ((algebraMap R T : (a : R) → T) r) : S ⊗[R] T)
      ((g : (a : T) → S ⊗[R] T) t : S ⊗[R] T) ∉
    J
e₁ : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)

Tactic:
rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht

Premises used: Algebra.smul_def, RingHom.map_mul, Ideal.mem_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 :
  HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) ((g : (a : T) → S ⊗[R] T) ((algebraMap R T : (a : R) → T) r) : S ⊗[R] T)
      ((g : (a : T) → S ⊗[R] T) t : S ⊗[R] T) ∉
    J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
⊢ False

Tactic:
ht (J.mul_mem_right _ H)

Premises used: Ideal.mul_mem_right
-- 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 :
  HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) ((g : (a : T) → S ⊗[R] T) ((algebraMap R T : (a : R) → T) r) : S ⊗[R] T)
      ((g : (a : T) → S ⊗[R] T) t : S ⊗[R] T) ∉
    J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : Membership.mem (α := S ⊗[R] T) J (1 ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
⊢ False

Tactic:
exact ht (J.mul_mem_right _ H)

Premises used: Ideal.mul_mem_right
-- 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
refine_2 :
  r • HMul.hMul (α := S ⊗[R] T) ((algebraMap R S : (a : R) → S) r ⊗ₜ[R] t : S ⊗[R] T) x = r • r • (1 ⊗ₜ[R] t * x)
⊢ HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) (1 ⊗ₜ[R] (r • t))
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) ((algebraMap R S : (a : R) → S) r) : S ⊗[R] T) *
      x =
    HMul.hMul (α := S ⊗[R] T) (β := S ⊗[R] T) (1 ⊗ₜ[R] (r • t))
      ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T)

Tactic:
simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul,
      one_mul, mul_one, id_apply, ← e]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, TensorProduct.tmul_smul, Algebra.TensorProduct.tmul_mul_tmul, RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, mul_one, 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)
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
refine_2 : r • (HSMul.hSMul (β := S) r 1 ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
refine_2₁ : r • (HSMul.hSMul (β := S ⊗[R] T) r (1 ⊗ₜ[R] t) * x) = r • r • (1 ⊗ₜ[R] t * x)
refine_2₂ refine_2₃ : r • r • (1 ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
⊢ r • HMul.hMul (α := S ⊗[R] T) ((algebraMap R S : (a : R) → S) r ⊗ₜ[R] t : S ⊗[R] T) x = r • r • (1 ⊗ₜ[R] t * x)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]

Premises used: smul_mul_assoc, Algebra.algebraMap_eq_smul_one, TensorProduct.smul_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 S)
⊢ SurjectiveOnStalks (R := T) (S := S ⊗[R] T)
    (RingHom.comp
      (AlgHom.toRingHom
        (Algebra.TensorProduct.algHomOfLinearMapTensorProduct
            (↑(TensorProduct.comm R T S) : T ⊗[R] S →ₛₗ[id R] S ⊗[R] T) ⋯ ⋯ :
          T ⊗[R] S →ₐ[R] S ⊗[R] T))
      (algebraMap T (T ⊗[R] S)))

Tactic:
(surjectiveOnStalks_of_surjective (Algebra.TensorProduct.comm R T S).surjective).comp
      (hf.baseChange (S := T))

Premises used: RingHom.SurjectiveOnStalks.baseChange, RingHom.surjectiveOnStalks_of_surjective, Algebra.TensorProduct.comm, RingHom.SurjectiveOnStalks.comp, AlgEquiv.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
inst_3 : Algebra R T
inst_4 : Algebra R S
hf : SurjectiveOnStalks (algebraMap R S)
⊢ SurjectiveOnStalks (R := T) (S := S ⊗[R] T) (AlgHom.toRingHom Algebra.TensorProduct.includeRight)

Tactic:
convert!
    (surjectiveOnStalks_of_surjective (Algebra.TensorProduct.comm R T S).surjective).comp
      (hf.baseChange (S := T))

Premises used: RingHom.SurjectiveOnStalks.baseChange, RingHom.surjectiveOnStalks_of_surjective, Algebra.TensorProduct.comm, RingHom.SurjectiveOnStalks.comp, AlgEquiv.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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this : Algebra S S' := f.toAlgebra
⊢ IsScalarTower R S S'

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
change :
  SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))
⊢ SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T) : S ⊗[R] T →ₐ[R] S' ⊗[R] T))

Tactic:
change (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).SurjectiveOnStalks

Premises used: Algebra.TensorProduct.map, AlgHom.id, Algebra.ofId, AlgHom.toRingHom, RingHom.SurjectiveOnStalks
-- 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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
h :
  Eq (α := S ⊗[R] T →+* S' ⊗[R] T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))
    (AlgHom.toRingHom
      (AlgHom.comp
          ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
            S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
          (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
        S ⊗[R] T →ₐ[S] S' ⊗[R] T))
convert_to :
  SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T)
    (AlgHom.toRingHom
      (AlgHom.comp
          ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
            S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
          (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
        S ⊗[R] T →ₐ[S] S' ⊗[R] T))
⊢ SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))

Tactic:
convert_to ((Algebra.TensorProduct.cancelBaseChange R S S S' T).toAlgHom.comp
    Algebra.TensorProduct.includeRight).SurjectiveOnStalks

Premises used: AlgEquiv.toAlgHom, AlgHom.toRingHom, RingHom.SurjectiveOnStalks, Algebra.TensorProduct.cancelBaseChange, AlgHom.comp, Algebra.TensorProduct.includeRight
-- 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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
h :
  Eq (α := S ⊗[R] T →ₐ[S] S' ⊗[R] T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T)
    (AlgHom.comp
        ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
          S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
        (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
      S ⊗[R] T →ₐ[S] S' ⊗[R] T)
⊢ Eq (α := S ⊗[R] T →+* S' ⊗[R] T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))
    (AlgHom.toRingHom
      (AlgHom.comp
          ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
            S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
          (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
        S ⊗[R] T →ₐ[S] S' ⊗[R] T))

Tactic:
congr
-- 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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
h :
  ∀ (x : T),
    Eq (α := S' ⊗[R] T)
      ((AlgHom.comp (B := S ⊗[R] T)
              (AlgHom.restrictScalars R
                (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))
              Algebra.TensorProduct.includeRight :
            (a : T) → S' ⊗[R] T)
          x :
        S' ⊗[R] T)
      ((AlgHom.comp (B := S ⊗[R] T)
              (AlgHom.restrictScalars R
                (AlgHom.comp
                    ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
                      S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
                    (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
                  S ⊗[R] T →ₐ[S] S' ⊗[R] T))
              Algebra.TensorProduct.includeRight :
            (a : T) → S' ⊗[R] T)
          x :
        S' ⊗[R] T)
⊢ Eq (α := S ⊗[R] T →ₐ[S] S' ⊗[R] T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T)
    (AlgHom.comp
        ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
          S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
        (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
      S ⊗[R] T →ₐ[S] S' ⊗[R] T)

Tactic:
ext
-- 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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
x : T
⊢ Eq (α := S' ⊗[R] T)
    ((AlgHom.comp (B := S ⊗[R] T)
            (AlgHom.restrictScalars R
              (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))
            Algebra.TensorProduct.includeRight :
          (a : T) → S' ⊗[R] T)
        x :
      S' ⊗[R] T)
    ((AlgHom.comp (B := S ⊗[R] T)
            (AlgHom.restrictScalars R
              (AlgHom.comp
                  ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
                    S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
                  (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
                S ⊗[R] T →ₐ[S] S' ⊗[R] T))
            Algebra.TensorProduct.includeRight :
          (a : T) → S' ⊗[R] T)
        x :
      S' ⊗[R] T)

Tactic:
simp
-- 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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T)
    (AlgHom.toRingHom
      (AlgHom.comp
          ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
            S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
          (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
        S ⊗[R] T →ₐ[S] S' ⊗[R] T))

Tactic:
(Algebra.TensorProduct.cancelBaseChange R S S S' T).toRingEquiv.surjectiveOnStalks.comp
    Hf.baseChange'

Premises used: AlgEquiv.toRingEquiv, RingEquiv.surjectiveOnStalks, Algebra.TensorProduct.cancelBaseChange, RingHom.SurjectiveOnStalks.comp, RingHom.SurjectiveOnStalks.baseChange'
-- 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
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T)
    (AlgHom.toRingHom
      (AlgHom.comp
          ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T) : S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T) :
            S' ⊗[S] (S ⊗[R] T) →ₐ[S] S' ⊗[R] T)
          (Algebra.TensorProduct.includeRight : S ⊗[R] T →ₐ[S] S' ⊗[S] (S ⊗[R] T)) :
        S ⊗[R] T →ₐ[S] S' ⊗[R] T))

Tactic:
exact (Algebra.TensorProduct.cancelBaseChange R S S S' T).toRingEquiv.surjectiveOnStalks.comp
    Hf.baseChange'

Premises used: AlgEquiv.toRingEquiv, RingEquiv.surjectiveOnStalks, Algebra.TensorProduct.cancelBaseChange, RingHom.SurjectiveOnStalks.comp, RingHom.SurjectiveOnStalks.baseChange'
-- 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
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
⊢ SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T')
    (RingHom.comp (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T'))
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R T' S)))
        (RingHom.comp (AlgHom.toRingHom (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S))
          (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R S T))))))

Tactic:
RingHom.SurjectiveOnStalks.tensorProductMap_id (T := T') Hf |>.comp <|
      (Algebra.TensorProduct.comm _ _ _).toRingEquiv.surjectiveOnStalks |>.comp <|
        RingHom.SurjectiveOnStalks.tensorProductMap_id (T := S) Hg |>.comp <|
          (Algebra.TensorProduct.comm _ _ _).toRingEquiv.surjectiveOnStalks

Premises used: RingEquiv.surjectiveOnStalks, RingHom.SurjectiveOnStalks.comp, _private.0.RingHom.SurjectiveOnStalks.tensorProductMap_id
-- 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
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
h :
  Eq (α := S ⊗[R] T →+* S' ⊗[R] T') (AlgHom.toRingHom (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
    (RingHom.comp (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T'))
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R T' S)))
        (RingHom.comp (AlgHom.toRingHom (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S))
          (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R S T))))))
⊢ SurjectiveOnStalks (R := S ⊗[R] T) (S := S' ⊗[R] T')
    (AlgHom.toRingHom (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T'))

Tactic:
convert!
    RingHom.SurjectiveOnStalks.tensorProductMap_id (T := T') Hf |>.comp <|
      (Algebra.TensorProduct.comm _ _ _).toRingEquiv.surjectiveOnStalks |>.comp <|
        RingHom.SurjectiveOnStalks.tensorProductMap_id (T := S) Hg |>.comp <|
          (Algebra.TensorProduct.comm _ _ _).toRingEquiv.surjectiveOnStalks

Premises used: RingEquiv.surjectiveOnStalks, RingHom.SurjectiveOnStalks.comp, _private.0.RingHom.SurjectiveOnStalks.tensorProductMap_id
-- 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
S' : Type u_4
T' : Type u_5
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
g : T →ₐ[R] T'
Hg : g.SurjectiveOnStalks
h :
  Eq (α := S ⊗[R] T →+* S' ⊗[R] T')
    (↑(Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T') : S ⊗[R] T →+* S' ⊗[R] T')
    (↑(AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T')
            (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : T' ⊗[R] S →ₐ[R] S ⊗[R] T')
                (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S)
                  ((↑(Algebra.TensorProduct.comm R S T) : S ⊗[R] T →ₐ[R] T ⊗[R] S) : S ⊗[R] T →ₐ[R] T ⊗[R] S)) :
              S ⊗[R] T →ₐ[R] S ⊗[R] T') :
          S ⊗[R] T →ₐ[R] S' ⊗[R] T') :
      S ⊗[R] T →+* S' ⊗[R] T')
⊢ Eq (α := S ⊗[R] T →+* S' ⊗[R] T') (AlgHom.toRingHom (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
    (RingHom.comp (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T') : S ⊗[R] T' →ₐ[R] S' ⊗[R] T'))
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R T' S)))
        (RingHom.comp (AlgHom.toRingHom (Algebra.TensorProduct.map g (AlgHom.id R S) : T ⊗[R] S →ₐ[R] T' ⊗[R] S))
          (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (Algebra.TensorProduct.comm R S T))))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_toRingHom, AlgEquiv.toRingEquiv_toRingHom, AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe