awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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)
have 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
Tactic: refine surjectiveOnStalks_of_exists_div fun s ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M s
Cleared hypotheses: 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
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
⊢ 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)
have 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)
Tactic: rw [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
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨t, r, a, ht, e⟩ := hf.exists_mul_eq_tmul x (J.comap g) inferInstance
-- 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)
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)
have refine_1 : ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) ((algebraMap R S : (a : R) → S) r) : S ⊗[R] T) ∉ J
Tactic: refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩
-- 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)
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
⊢ ∃ (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)
have 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)
Tactic: refine ⟨a, algebraMap _ _ r, 1 ⊗ₜ (r • t), ht, ?_, ?_⟩
-- 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
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)
⊢ False
have H₁ : 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
Cleared hypotheses: H
-- 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
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)
⊢ False
have 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
Tactic: rw [Ideal.mem_comap, Algebra.smul_def, g.map_mul] at ht
Cleared hypotheses: ht, e, 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
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
⊢ 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)
have 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)
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]
-- 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)
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
⊢ 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)
have refine_2 : r • (HSMul.hSMul (β := S) r 1 ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]
-- 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)
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)
⊢ 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)
have refine_2₁ : r • (HSMul.hSMul (β := S ⊗[R] T) r (1 ⊗ₜ[R] t) * x) = r • r • (1 ⊗ₜ[R] t * x)
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]
-- 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)
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)
⊢ 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)
have refine_2₂ : r • r • (1 ⊗ₜ[R] t * x) = r • r • (1 ⊗ₜ[R] t * x)
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]
-- 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
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
⊢ 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))
have this₁ : IsScalarTower R S S'
Tactic: have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- 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
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 (Algebra.TensorProduct.map f (AlgHom.id R T) : S ⊗[R] T →ₐ[R] S' ⊗[R] T))
have 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))
Tactic: change (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).SurjectiveOnStalks
-- 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
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 (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) : S ⊗[R] T →ₐ[S] S' ⊗[R] T))
have 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))
Tactic: convert_to ((Algebra.TensorProduct.cancelBaseChange R S S S' T).toAlgHom.comp
    Algebra.TensorProduct.includeRight).SurjectiveOnStalks
-- 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
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))
⊢ 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))
have 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))
Tactic: convert_to ((Algebra.TensorProduct.cancelBaseChange R S S S' T).toAlgHom.comp
    Algebra.TensorProduct.includeRight).SurjectiveOnStalks
-- 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
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'
⊢ 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))
have 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)
Tactic: congr
-- 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
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'
⊢ 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)
have 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)
Tactic: ext
-- 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
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')
    (AlgHom.toRingHom (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] S' ⊗[R] T'))
have 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))))))
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
-- 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
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
⊢ 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))))))
have 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')
Tactic: simp only [AlgHom.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, ← AlgEquiv.toAlgHom_toRingHom, ← AlgHom.comp_toRingHom]
-- 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
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
⊢ 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')
have h : Eq (α := S ⊗[R] T →ₐ[R] S' ⊗[R] T') (Algebra.TensorProduct.map f g : S ⊗[R] T →ₐ[R] 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')
Tactic: congr