awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
m : M
x : ↥f.ker
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (((((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f) :
                  M →ₗ[S] ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
                (a : M) → ↥f.ker →ₗ[R] M ⊗[R] ↥f.ker)
              m :
            ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
          (a : ↥f.ker) → M ⊗[R] ↥f.ker)
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (((((AlgebraTensorModule.curry id : M →ₗ[S] ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
                (a : M) → ↥f.ker →ₗ[R] M ⊗[R] ↥f.ker)
              m :
            ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
          (a : ↥f.ker) → M ⊗[R] ↥f.ker)
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
have a : Eq (α := M ⊗[R] N)
  ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      (((((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f) :
                  M →ₗ[S] ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
                (a : M) → ↥f.ker →ₗ[R] M ⊗[R] ↥f.ker)
              m :
            ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
          (a : ↥f.ker) → M ⊗[R] ↥f.ker)
        x) :
    M ⊗[R] N)
  ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      (((((AlgebraTensorModule.curry id : M →ₗ[S] ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
                (a : M) → ↥f.ker →ₗ[R] M ⊗[R] ↥f.ker)
              m :
            ↥f.ker →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) :
          (a : ↥f.ker) → M ⊗[R] ↥f.ker)
        x) :
    M ⊗[R] N)
Tactic: apply (Module.Flat.lTensor_preserves_injective_linearMap (ker f).subtype
        (ker f).injective_subtype)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
⊢ Eq (α :=
    ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
              f :
            M ⊗[R] N →ₗ[S] M ⊗[R] P)
          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
              g :
            M ⊗[R] N →ₗ[S] M ⊗[R] P)) →ₗ[S]
      ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
              f :
            M ⊗[R] N →ₗ[S] M ⊗[R] P)
          (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
              g :
            M ⊗[R] N →ₗ[S] M ⊗[R] P)))
    (tensorEqLocus S M f g ∘ₗ tensorEqLocusInv S M f g) id
have h : ∀
  (x :
    ↥(eqLocus (F := M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            f :
          M ⊗[R] N →ₗ[S] M ⊗[R] P)
        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
              (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
            g :
          M ⊗[R] N →ₗ[S] M ⊗[R] P))),
  Eq (α := M ⊗[R] N)
    (↑((tensorEqLocus S M f g ∘ₗ tensorEqLocusInv S M f g :
            (a :
                ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                    ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g))) →
              ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                  ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
          x) :
      M ⊗[R] N)
    (↑((id :
            (a :
                ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                    ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g))) →
              ↥(eqLocus ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f)
                  ((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) g)))
          x) :
      M ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
    (tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g :
      TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
    (id : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
have a : ∀ (m : M) (x : ↥(eqLocus f g)),
  Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
    (((((AlgebraTensorModule.curry (tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g) :
                  M →ₗ[S] ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
                (a : M) → ↥(eqLocus f g) →ₗ[R] M ⊗[R] ↥(eqLocus f g))
              m :
            ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
          (a : ↥(eqLocus f g)) → M ⊗[R] ↥(eqLocus f g))
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
    (((((AlgebraTensorModule.curry id : M →ₗ[S] ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
                (a : M) → ↥(eqLocus f g) →ₗ[R] M ⊗[R] ↥(eqLocus f g))
              m :
            ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
          (a : ↥(eqLocus f g)) → M ⊗[R] ↥(eqLocus f g))
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
Tactic: ext m x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
inst_11 : Module.Flat R M
m : M
x : ↥(eqLocus f g)
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
    (((((AlgebraTensorModule.curry (tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g) :
                  M →ₗ[S] ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
                (a : M) → ↥(eqLocus f g) →ₗ[R] M ⊗[R] ↥(eqLocus f g))
              m :
            ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
          (a : ↥(eqLocus f g)) → M ⊗[R] ↥(eqLocus f g))
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
    (((((AlgebraTensorModule.curry id : M →ₗ[S] ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
                (a : M) → ↥(eqLocus f g) →ₗ[R] M ⊗[R] ↥(eqLocus f g))
              m :
            ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
          (a : ↥(eqLocus f g)) → M ⊗[R] ↥(eqLocus f g))
        x :
      TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g))
have a : Eq (α := M ⊗[R] N)
  ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      (((((AlgebraTensorModule.curry (tensorEqLocusInv S M f g ∘ₗ tensorEqLocus S M f g) :
                  M →ₗ[S] ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
                (a : M) → ↥(eqLocus f g) →ₗ[R] M ⊗[R] ↥(eqLocus f g))
              m :
            ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
          (a : ↥(eqLocus f g)) → M ⊗[R] ↥(eqLocus f g))
        x) :
    M ⊗[R] N)
  ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      (((((AlgebraTensorModule.curry id :
                  M →ₗ[S] ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
                (a : M) → ↥(eqLocus f g) →ₗ[R] M ⊗[R] ↥(eqLocus f g))
              m :
            ↥(eqLocus f g) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) :
          (a : ↥(eqLocus f g)) → M ⊗[R] ↥(eqLocus f g))
        x) :
    M ⊗[R] N)
Tactic: apply (Module.Flat.lTensor_preserves_injective_linearMap (eqLocus f g).subtype
        (eqLocus f g).injective_subtype)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_4
P : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
g : M →ₗ[R] N
hg : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑g : (a : M) → N)
H : Function.Exact.{u_3, u_4, u_5} (M := M) (N := N) (P := P) (⇑g : (a : M) → N) (⇑f : (a : N) → P)
A : Type u_6
inst_8 : AddCommGroup A
inst_9 : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun (a : A) ↦ a
⊢ Function.Injective (α := A ⊗[R] M) (β := A ⊗[R] N) (⇑(lTensor A g) : (a : A ⊗[R] M) → A ⊗[R] N)
have hπ : Function.Surjective (α := Q) (β := A) (⇑π : (a : Q) → A)
Tactic: have hπ : Function.Surjective π := Finsupp.linearCombination_surjective _ Function.surjective_id
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_4
P : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
g : M →ₗ[R] N
hg : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑g : (a : M) → N)
H : Function.Exact.{u_3, u_4, u_5} (M := M) (N := N) (P := P) (⇑g : (a : M) → N) (⇑f : (a : N) → P)
A : Type u_6
inst_8 : AddCommGroup A
inst_9 : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun (a : A) ↦ a
hπ : Function.Surjective (α := Q) (β := A) (⇑π : (a : Q) → A)
K : Submodule R Q := π.ker
⊢ Function.Exact (M := Unit) (N := sorry) (P := sorry) (⇑0 : (a : Unit) → sorry) (⇑sorry : (a : sorry) → sorry)
have simpa : Function.Injective (α := sorry) (β := sorry) (⇑sorry : (a : sorry) → sorry)
Tactic: simpa using Module.Flat.rTensor_preserves_injective_linearMap _ K.subtype_injective
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
f g : A →ₐ[R] B
x : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
⊢ Eq (α := T ⊗[R] A)
    ((↑((tensorEqualizerAux S T f g :
              (a : T ⊗[R] ↥(equalizer f g)) →
                ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                    (Algebra.TensorProduct.map (AlgHom.id S T) g)))
            x) :
        T ⊗[R] A) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
            TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
          (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
        x :
      T ⊗[R] A)
have zero : Eq (α := T ⊗[R] A)
  (↑((tensorEqualizerAux S T f g :
          (a : T ⊗[R] ↥(equalizer f g)) →
            ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g)))
        0) :
    T ⊗[R] A)
  (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
        TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
      (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
    0)
Tactic: induction x with
  | zero => rfl
  | tmul => rfl
  | add x y hx hy => simp [hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
f g : A →ₐ[R] B
x : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
zero :
  Eq (α := T ⊗[R] A)
    (↑((tensorEqualizerAux S T f g :
            (a : T ⊗[R] ↥(equalizer f g)) →
              ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f) (Algebra.TensorProduct.map (AlgHom.id S T) g)))
          0) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
          TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
        (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
      0)
⊢ Eq (α := T ⊗[R] A)
    ((↑((tensorEqualizerAux S T f g :
              (a : T ⊗[R] ↥(equalizer f g)) →
                ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                    (Algebra.TensorProduct.map (AlgHom.id S T) g)))
            x) :
        T ⊗[R] A) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
            TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
          (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
        x :
      T ⊗[R] A)
have tmul : ∀ (x : T) (y : ↥(equalizer f g)),
  Eq (α := T ⊗[R] A)
    ((↑((tensorEqualizerAux S T f g :
              (a : T ⊗[R] ↥(equalizer f g)) →
                ↥(equalizer (Algebra.TensorProduct.map (AlgHom.id S T) f)
                    (Algebra.TensorProduct.map (AlgHom.id S T) g)))
            (x ⊗ₜ[R] y)) :
        T ⊗[R] A) :
      T ⊗[R] A)
    (((Algebra.TensorProduct.map (AlgHom.id S T) (Subalgebra.val (equalizer f g)) :
            TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g) →ₐ[S] T ⊗[R] A) :
          (a : T ⊗[R] ↥(equalizer f g)) → T ⊗[R] A)
        (x ⊗ₜ[R] y) :
      T ⊗[R] A)
Tactic: induction x with
  | zero => rfl
  | tmul => rfl
  | add x y hx hy => simp [hx, hy]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
f g : A →ₐ[R] B
inst_11 : Module.Flat R T
h₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 : A ⊗[R] S ≃ₐ[R] S ⊗[R] A := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] TensorProduct.{u_1, u_4, u_2} R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  LinearEquiv.restrictScalars R (S := R)
    (LinearMap.kerLTensorEquivOfSurjective.{u_1, u_2, u_3, u_4} (R := R) (N := S) (P := T)
      (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S T)) h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (LinearEquiv.symm
              (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A) :
            TensorProduct.{u_1, u_2, u_4} R (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A ≃ₗ[S]
              ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A)) ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (F := S →+* T) (algebraMap S T)))
            (↑ePp.symm : S ⊗[R] A ≃ₗ[S] A ⊗[R] S) :
          ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A) ≃ₗ[S]
            ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (A ⊗[R] S)) ≪≫ₗ
    LinearEquiv.restrictScalars R
      (_root_.TensorProduct.comm S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) (A ⊗[R] S))
r' : A ⊗[R] S
x : A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
⊢ (↑e₄'.symm : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) →ₗ[R] ↥(RingHom.ker φ)).toFun (r' • x) =
    HSMul.hSMul (α := A ⊗[R] S) ((RingHom.id (A ⊗[R] S) : (a : A ⊗[R] S) → A ⊗[R] S) r' : A ⊗[R] S)
      ((↑e₄'.symm : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) →ₗ[R] ↥(RingHom.ker φ)).toFun x)
have dsimp : (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (r' • x) =
  HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
    ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) x : ↥(RingHom.ker φ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
f g : A →ₐ[R] B
inst_11 : Module.Flat R T
h₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 : A ⊗[R] S ≃ₐ[R] S ⊗[R] A := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] TensorProduct.{u_1, u_4, u_2} R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  LinearEquiv.restrictScalars R (S := R)
    (LinearMap.kerLTensorEquivOfSurjective.{u_1, u_2, u_3, u_4} (R := R) (N := S) (P := T)
      (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S T)) h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (LinearEquiv.symm
              (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A) :
            TensorProduct.{u_1, u_2, u_4} R (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A ≃ₗ[S]
              ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A)) ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (F := S →+* T) (algebraMap S T)))
            (↑ePp.symm : S ⊗[R] A ≃ₗ[S] A ⊗[R] S) :
          ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A) ≃ₗ[S]
            ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (A ⊗[R] S)) ≪≫ₗ
    LinearEquiv.restrictScalars R
      (_root_.TensorProduct.comm S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
      (HSMul.hSMul (α := A ⊗[R] S) (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) (r ⊗ₜ[R] s)
        (x ⊗ₜ[R] z ⊗ₜ[S] y)) =
    HSMul.hSMul (α := A ⊗[R] S) (β := ↥(RingHom.ker φ)) (r ⊗ₜ[R] s)
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[R] z ⊗ₜ[S] y) :
        ↥(RingHom.ker φ))
have tmul : (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
    (HSMul.hSMul (α := A ⊗[R] S) (β := A ⊗[R] S) (r ⊗ₜ[R] s) (x ⊗ₜ[R] z) ⊗ₜ[S] y) =
  HSMul.hSMul (α := A ⊗[R] S) (β := ↥(RingHom.ker φ)) (r ⊗ₜ[R] s)
    ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[R] z ⊗ₜ[S] y) :
      ↥(RingHom.ker φ))
Tactic: rw [smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Equalizer (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
f g : A →ₐ[R] B
inst_11 : Module.Flat R T
h₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 : A ⊗[R] S ≃ₐ[R] S ⊗[R] A := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] TensorProduct.{u_1, u_4, u_2} R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  LinearEquiv.restrictScalars R (S := R)
    (LinearMap.kerLTensorEquivOfSurjective.{u_1, u_2, u_3, u_4} (R := R) (N := S) (P := T)
      (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S T)) h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (LinearEquiv.symm
              (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A) :
            TensorProduct.{u_1, u_2, u_4} R (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) A ≃ₗ[S]
              ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A)) ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (F := S →+* T) (algebraMap S T)))
            (↑ePp.symm : S ⊗[R] A ≃ₗ[S] A ⊗[R] S) :
          ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (S ⊗[R] A) ≃ₗ[S]
            ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ⊗[S] (A ⊗[R] S)) ≪≫ₗ
    LinearEquiv.restrictScalars R
      (_root_.TensorProduct.comm S (↥(RingHom.ker (F := S →+* T) (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ (↑((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
          (HSMul.hSMul (α := A ⊗[R] S) (β := A ⊗[R] S) (r ⊗ₜ[R] s) (x ⊗ₜ[R] z) ⊗ₜ[S] y)) :
      A ⊗[R] S) =
    (↑(HSMul.hSMul (α := A ⊗[R] S) (β := ↥(RingHom.ker φ)) (r ⊗ₜ[R] s)
          ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[R] z ⊗ₜ[S] y) :
            ↥(RingHom.ker φ))) :
      A ⊗[R] S)
have tmul : (↑((e₃.symm :
          (a : A ⊗[R] ↥(RingHom.ker (algebraMap S T))) →
            ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))))
        ((r * x) ⊗ₜ[R] ((s * z) • y))) :
    A ⊗[R] S) =
  HMul.hMul (α := A ⊗[R] S) (r ⊗ₜ[R] s)
    (↑((e₃.symm :
            (a : A ⊗[R] ↥(RingHom.ker (algebraMap S T))) →
              ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))))
          (x ⊗ₜ[R] (z • y))) :
      A ⊗[R] S)
Tactic: dsimp [e₄', ePp, φ]