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
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
⊢ (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
      (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' 0) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) 0)

Tactic:
simp only [smul_zero, LinearEquiv.map_zero]

Premises used: LinearEquiv.map_zero, smul_zero
-- 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 y : A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
h :
  (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 φ))
h_1 :
  (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (r' • y) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) y : ↥(RingHom.ker φ))
⊢ (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (r' • (x + y)) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x + y) : ↥(RingHom.ker φ))

Tactic:
simp only [smul_add, LinearEquiv.map_add, *]

Premises used: LinearEquiv.map_add, smul_add
-- 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
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
⊢ (e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ))
      (HSMul.hSMul (β := A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))) r' (0 ⊗ₜ[S] y)) =
    HSMul.hSMul (β := ↥(RingHom.ker φ)) r'
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (0 ⊗ₜ[S] y) :
        ↥(RingHom.ker φ))

Tactic:
simp only [zero_tmul, smul_zero, LinearEquiv.map_zero]

Premises used: LinearEquiv.map_zero, smul_zero, TensorProduct.zero_tmul
-- 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))
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
x : A
z : 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))) 0
        (x ⊗ₜ[R] z ⊗ₜ[S] y)) =
    HSMul.hSMul (α := A ⊗[R] S) (β := ↥(RingHom.ker φ)) 0
      ((e₄'.symm : (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) → ↥(RingHom.ker φ)) (x ⊗ₜ[R] z ⊗ₜ[S] y) :
        ↥(RingHom.ker φ))

Tactic:
simp only [zero_smul, LinearEquiv.map_zero]

Premises used: LinearEquiv.map_zero, zero_smul
-- 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))
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
x : A
z : S
r : A
s : S
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 φ))
⊢ (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 φ))

Tactic:
rw [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- 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))
y : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
x : A
z : S
r : A
s : S
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)
⊢ (↑((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)

Tactic:
dsimp [e₄', ePp, φ]
-- 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))
e₄ : A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T)) ≃ₗ[A ⊗[R] S] ↥(RingHom.ker φ) :=
  let __spread.0 := e₄'.symm;
  { toAddHom := (↑__spread.0 : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) →ₗ[R] ↥(RingHom.ker φ)).toAddHom,
    map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ ↥(RingHom.ker (F := A ⊗[R] S →ₐ[A] A ⊗[R] T)
        (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T) : A ⊗[R] S →ₐ[A] A ⊗[R] T)) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (F := S →+* T) (algebraMap S T))

Tactic:
exact e₄.symm

Premises used: LinearEquiv.symm
-- 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
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : Module.Flat R T
h₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
x : A
y : S
z : ↥(RingHom.ker (F := S →+* T) (algebraMap S T))
⊢ Eq (α := A ⊗[R] S)
    (↑((LinearEquiv.symm (kerTensorProductMapIdToAlgHomEquiv R S T A h₁) :
            (a : A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))) →
              ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))))
          (x ⊗ₜ[R] y ⊗ₜ[S] z)) :
      A ⊗[R] S)
    (x ⊗ₜ[R] (y * (↑z : S)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : Fintype ι
f : ι → R
x : ι → M
⊢ IsTrivialRelation f x ↔ VanishesTrivially R f x

Tactic:
simp only [IsTrivialRelation, VanishesTrivially, smul_eq_mul, mul_comm]

Premises used: TensorProduct.VanishesTrivially, mul_comm, smul_eq_mul, Module.IsTrivialRelation
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst_4 : Fintype κ
e : κ ≃ ι
simp_rw :
  VanishesTrivially.{u_1, u_1, u_2, u_4} R (ι := κ) (f ∘ (⇑e : (a : κ) → ι)) (x ∘ (⇑e : (a : κ) → ι)) ↔
    VanishesTrivially R f x
⊢ IsTrivialRelation.{u_1, u_2, u_4} (ι := κ) (f ∘ (⇑e : (a : κ) → ι)) (x ∘ (⇑e : (a : κ) → ι)) ↔ IsTrivialRelation f x

Tactic:
simp_rw [isTrivialRelation_iff_vanishesTrivially, e.vanishesTrivially_comp]

Premises used: Equiv.vanishesTrivially_comp, Module.isTrivialRelation_iff_vanishesTrivially
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : Fintype ι
f : ι → R
x : ι → M
h : IsTrivialRelation f x
⊢ Eq.{u_2 + 1} (α := M) (∑ i : ι, f i • x i) 0

Tactic:
simpa using
    congr_arg (TensorProduct.lid R M) <|
      sum_tmul_eq_zero_of_vanishesTrivially R (isTrivialRelation_iff_vanishesTrivially.mp h)

Premises used: TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially, congr_arg, Module.isTrivialRelation_iff_vanishesTrivially, Iff.mp, TensorProduct.lid, DFunLike.coe
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ ∀ (I : Ideal R),
    Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
      (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M)

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M)

Tactic:
tfae_have 1 ↔ 2 := iff_rTensor_injective'

Premises used: Module.Flat.iff_rTensor_injective'