awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Equalizer
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)
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)
⊢ 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:
apply (Module.Flat.lTensor_preserves_injective_linearMap (eqLocus f g).subtype
        (eqLocus f g).injective_subtype)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, Submodule.injective_subtype, LinearMap.eqLocus, Submodule.subtype
-- Module: Mathlib.RingTheory.Flat.Equalizer
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 (α := 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:
simp
-- Module: Mathlib.RingTheory.Flat.Equalizer
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
x : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)
⊢ 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)))
    ((tensorEqLocusEquiv S M f g :
          (a : M ⊗[R] ↥(eqLocus f 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 :
      ↥(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 :
          (a : M ⊗[R] ↥(eqLocus f 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 :
      ↥(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)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Flat.Equalizer
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
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))
⊢ (lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      ((LinearEquiv.symm (tensorEqLocusEquiv 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))) →
            M ⊗[R] ↥(eqLocus f g))
        x) =
    (↑x : M ⊗[R] N)

Tactic:
lTensor_eqLocus_subtype_tensorEqLocusInv S M f g x

Premises used: _private.0.LinearMap.lTensor_eqLocus_subtype_tensorEqLocusInv, Classical.choose
-- Module: Mathlib.RingTheory.Flat.Equalizer
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.Surjective (α := Q) (β := A) (⇑π : (a : Q) → A)

Tactic:
have hπ : Function.Surjective π := Finsupp.linearCombination_surjective _ Function.surjective_id
-- Module: Mathlib.RingTheory.Flat.Equalizer
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
simpa : Function.Injective (α := sorry) (β := sorry) (⇑sorry : (a : sorry) → sorry)
⊢ Function.Exact (M := Unit) (N := sorry) (P := sorry) (⇑0 : (a : Unit) → sorry) (⇑sorry : (a : sorry) → sorry)

Tactic:
simpa using Module.Flat.rTensor_preserves_injective_linearMap _ K.subtype_injective

Premises used: Submodule.subtype_injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Equalizer
Goal:
R : Type u_1
inst : CommRing R
N : Type u_4
P : Type u_5
inst_1 : AddCommGroup N
inst_2 : AddCommGroup P
inst_3 : Module R N
inst_4 : Module R P
inst_5 : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective.{u_4 + 1, u_5 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
A : Type u_6
inst_6 : AddCommGroup A
inst_7 : Module R A
a : A
y : ↥f.ker
⊢ Eq (α := A ⊗[R] N)
    (↑((LinearEquiv.symm (f.kerLTensorEquivOfSurjective hf A) : (a : A ⊗[R] ↥f.ker) → ↥(lTensor A f).ker) (a ⊗ₜ[R] y)) :
      A ⊗[R] N)
    (a ⊗ₜ[R] (↑y : N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Flat.Equalizer
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
⊢ AddHomClass (A →ₐ[R] B) A B

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Flat.Equalizer
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
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.Flat.Equalizer
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 : 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:
rfl
-- Module: Mathlib.RingTheory.Flat.Equalizer
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 y : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
hx :
  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)
hy :
  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)))
            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)
        y :
      T ⊗[R] A)
⊢ 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 + 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 + y) :
      T ⊗[R] A)

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.Flat.Equalizer
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 y : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
⊢ ((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 * y) =
    (↑(HMul.hMul (α :=
          ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
          (β :=
          ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
              (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
          ((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 :
            ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
          ((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)))
              y :
            ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
                (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))) :
      T ⊗[R] A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Equalizer
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)
    ((↑((tensorEqualizer 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)

Tactic:
AlgHom.coe_tensorEqualizerAux S T f g x

Premises used: _private.0.AlgHom.coe_tensorEqualizerAux
-- Module: Mathlib.RingTheory.Flat.Equalizer
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
x : TensorProduct.{u_1, u_3, u_4} R T ↥(equalizer f g)
⊢ Eq (α :=
    ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B) (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
        (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
    ((tensorEqualizerEquiv 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 :
      ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B) (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
          (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))
    ((tensorEqualizer 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 :
      ↥(equalizer (F := T ⊗[R] A →ₐ[S] T ⊗[R] B) (Algebra.TensorProduct.map (AlgHom.id S T) f : T ⊗[R] A →ₐ[S] T ⊗[R] B)
          (Algebra.TensorProduct.map (AlgHom.id S T) g : T ⊗[R] A →ₐ[S] T ⊗[R] B)))

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Quotient.liftOn', Set.Mem, AddCon.liftOn, setOf, SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RingTheory.Flat.Equalizer
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))
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 φ))
⊢ (↑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)

Tactic:
dsimp