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
⊢ ∀
    (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))),
    Membership.mem (α := M ⊗[R] N) (γ := Submodule S (M ⊗[R] N))
      (range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)) (τ₁₂ := RingHom.id S)
        (((AlgebraTensorModule.lTensor S M :
              (↥(eqLocus f g) →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
            (a : ↥(eqLocus f g) →ₗ[R] N) → M ⊗[R] ↥(eqLocus f g) →ₗ[S] M ⊗[R] N)
          (Submodule.subtype (eqLocus f g))))
      ((Submodule.subtype
              (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)) :
            (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] N)
          x :
        M ⊗[R] N)

Tactic:
simp [Module.Flat.eqLocus_lTensor_eq]

Premises used: Module.Flat.eqLocus_lTensor_eq
-- 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))
rw :
  ((((AlgebraTensorModule.lTensor S M :
                (↥(eqLocus f g) →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
              (a : ↥(eqLocus f g) →ₗ[R] N) → M ⊗[R] ↥(eqLocus f g) →ₗ[S] M ⊗[R] N)
            (Submodule.subtype (eqLocus f g)) :
          TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
        (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      ((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))) →
            M ⊗[R] ↥(eqLocus f g))
        x) =
    (↑x : M ⊗[R] N)
⊢ (lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      ((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))) →
            M ⊗[R] ↥(eqLocus f g))
        x) =
    (↑x : M ⊗[R] N)

Tactic:
rw [← AlgebraTensorModule.coe_lTensor (A := S)]

Premises used: TensorProduct.AlgebraTensorModule.coe_lTensor
-- 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))
⊢ ((((AlgebraTensorModule.lTensor S M :
                (↥(eqLocus f g) →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
              (a : ↥(eqLocus f g) →ₗ[R] N) → M ⊗[R] ↥(eqLocus f g) →ₗ[S] M ⊗[R] N)
            (Submodule.subtype (eqLocus f g)) :
          TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g) →ₗ[S] M ⊗[R] N) :
        (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N)
      ((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))) →
            M ⊗[R] ↥(eqLocus f g))
        x) =
    (↑x : M ⊗[R] N)

Tactic:
simp [LinearMap.tensorEqLocusInv]

Premises used: LinearMap.tensorEqLocusInv
-- 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
h :
  ∀
    (x :
      ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((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))),
    Eq (α := M ⊗[R] N)
      (↑((tensorKer S M f ∘ₗ tensorKerInv S M f :
              (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) →
                ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
            x) :
        M ⊗[R] N)
      (↑((id :
              (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) →
                ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
            x) :
        M ⊗[R] N)
⊢ Eq (α :=
    ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((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)) →ₗ[S]
      ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((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)))
    (tensorKer S M f ∘ₗ tensorKerInv S M f) id

Tactic:
ext x
-- 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 :
  ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
      (((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))
⊢ Eq (α := M ⊗[R] N)
    (↑((tensorKer S M f ∘ₗ tensorKerInv S M f :
            (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) →
              ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          x) :
      M ⊗[R] N)
    (↑((id :
            (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) →
              ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          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
a :
  ∀ (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)
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (tensorKerInv S M f ∘ₗ tensorKer S M f :
      TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)
    (id : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker)

Tactic:
ext m x
-- 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 : ↥f.ker
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)
⊢ 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)

Tactic:
apply (Module.Flat.lTensor_preserves_injective_linearMap (ker f).subtype
        (ker f).injective_subtype)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, LinearMap.ker, Submodule.injective_subtype, 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 : ↥f.ker
⊢ 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:
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 : N →ₗ[R] P
inst_11 : Module.Flat R M
x : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker
⊢ Eq (α :=
    ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
        (((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)))
    ((tensorKerEquiv S M f :
          (a : M ⊗[R] ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
        x :
      ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((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)))
    ((tensorKer S M f :
          (a : M ⊗[R] ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
        x :
      ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
          (((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)))

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 : N →ₗ[R] P
inst_11 : Module.Flat R M
x :
  ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
      (((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))
⊢ (lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      ((LinearEquiv.symm (tensorKerEquiv S M f) :
          (a : ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker) → M ⊗[R] ↥f.ker)
        x) =
    (↑x : M ⊗[R] N)

Tactic:
lTensor_ker_subtype_tensorKerInv S M f x

Premises used: _private.0.LinearMap.lTensor_ker_subtype_tensorKerInv, Classical.choose
-- 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
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)
⊢ 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

Tactic:
ext
-- 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))
⊢ 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:
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
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))
⊢ 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))

Tactic:
ext m x