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
m : M
r : R
x : ↥(eqLocus f g)
⊢ Subtype.mk (p := fun (x : M ⊗[R] N) ↦
      Membership.mem (γ := Submodule S (M ⊗[R] N))
        (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))
        x)
      (m ⊗ₜ[R] (↑(r • x) : N)) ⋯ =
    HSMul.hSMul (α := R) (β :=
      ↥(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)))
      ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (x : M ⊗[R] N) ↦
        Membership.mem (γ := Submodule S (M ⊗[R] N))
          (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))
          x)
        (m ⊗ₜ[R] (↑x : 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
m : M
a : ↥f.ker
⊢ Membership.mem (γ := Submodule S (M ⊗[R] N))
    (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))
    (m ⊗ₜ[R] (↑a : 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
m : M
x y : ↥f.ker
⊢ Subtype.mk (p := fun (x : M ⊗[R] N) ↦
      Membership.mem (γ := Submodule S (M ⊗[R] N))
        (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))
        x)
      (m ⊗ₜ[R] (↑(x + y) : N)) ⋯ =
    HAdd.hAdd (α :=
      ↥(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)))
      (Subtype.mk (p := fun (x : M ⊗[R] N) ↦
        Membership.mem (γ := Submodule S (M ⊗[R] N))
          (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))
          x)
        (m ⊗ₜ[R] (↑x : N)) ⋯)
      (Subtype.mk (p := fun (x : M ⊗[R] N) ↦
        Membership.mem (γ := Submodule S (M ⊗[R] N))
          (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))
          x)
        (m ⊗ₜ[R] (↑y : N)) ⋯)

Tactic:
simp [tmul_add]

Premises used: TensorProduct.tmul_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
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
m : M
r : R
x : ↥f.ker
⊢ Subtype.mk (p := fun (x : M ⊗[R] N) ↦
      Membership.mem (γ := Submodule S (M ⊗[R] N))
        (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))
        x)
      (m ⊗ₜ[R] (↑(r • x) : N)) ⋯ =
    HSMul.hSMul (α := R) (β :=
      ↥(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)))
      ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (x : M ⊗[R] N) ↦
        Membership.mem (γ := Submodule S (M ⊗[R] N))
          (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))
          x)
        (m ⊗ₜ[R] (↑x : 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
r : S
x : M
y : ↥f.ker
⊢ Eq (α := M ⊗[R] N)
    (↑(({
              toFun := fun (a : ↥f.ker) ↦
                Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                  Membership.mem (γ := Submodule S (M ⊗[R] N))
                    (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))
                    x)
                  ((r • x) ⊗ₜ[R] (↑a : N)) ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          y) :
      M ⊗[R] N)
    (↑((HSMul.hSMul (α := S) (β :=
              ↥f.ker →ₗ[R]
                ↥(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)))
              ((RingHom.id S : (a : S) → S) r : S)
              {
                toFun := fun (a : ↥f.ker) ↦
                  Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                    Membership.mem (γ := Submodule S (M ⊗[R] N))
                      (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))
                      x)
                    (x ⊗ₜ[R] (↑a : N)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ :
                ↥f.ker →ₗ[R]
                  ↥(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)) } :
            (a : ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          y) :
      M ⊗[R] N)

Tactic:
simp [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
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
m : M
x : ↥f.ker
⊢ Eq (α := M ⊗[R] N)
    (↑((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)
          (m ⊗ₜ[R] x)) :
      M ⊗[R] N)
    (m ⊗ₜ[R] (↑x : N))

Tactic:
rfl

Premises used: TensorProduct.tmul, 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
x : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker
zero :
  Eq (α := M ⊗[R] N)
    (↑((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)
          0) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) 0)
tmul :
  ∀ (x : M) (y : ↥f.ker),
    Eq (α := M ⊗[R] N)
      ((↑((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 ⊗ₜ[R] y)) :
          M ⊗[R] N) :
        M ⊗[R] N)
      ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
add :
  ∀ (x y : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker),
    Eq (α := M ⊗[R] N)
        ((↑((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) :
            M ⊗[R] N) :
          M ⊗[R] N)
        ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N) →
      Eq (α := M ⊗[R] N)
          ((↑((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)
                  y) :
              M ⊗[R] N) :
            M ⊗[R] N)
          ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) y : M ⊗[R] N) →
        Eq (α := M ⊗[R] N)
          ((↑((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 + y)) :
              M ⊗[R] N) :
            M ⊗[R] N)
          ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x + y) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    ((↑((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) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N)

Tactic:
induction 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 : N →ₗ[R] P
⊢ Eq (α := M ⊗[R] N)
    (↑((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)
          0) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) 0)

Tactic:
simp_all
-- 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
x : M
y : ↥f.ker
⊢ Eq (α := M ⊗[R] N)
    ((↑((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 ⊗ₜ[R] y)) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)

Tactic:
simp_all
-- 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
x y : TensorProduct.{u_1, u_3, u_4} R M ↥f.ker
h :
  Eq (α := M ⊗[R] N)
    ((↑((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) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) x : M ⊗[R] N)
h_1 :
  Eq (α := M ⊗[R] N)
    ((↑((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)
            y) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) y : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    ((↑((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 + y)) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N) (x + y) : M ⊗[R] N)

Tactic:
simp_all
-- 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
m : M
x : ↥(eqLocus f g)
⊢ Eq (α := M ⊗[R] N)
    (↑((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)))
          (m ⊗ₜ[R] x)) :
      M ⊗[R] N)
    (m ⊗ₜ[R] (↑x : N))

Tactic:
rfl

Premises used: TensorProduct.tmul, 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
⊢ Eq (α := M ⊗[R] N)
    (↑((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)))
          0) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) 0)

Tactic:
simp_all
-- 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
x : M
y : ↥(eqLocus f g)
⊢ Eq (α := M ⊗[R] N)
    ((↑((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 ⊗ₜ[R] y)) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)

Tactic:
simp_all
-- 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
x y : TensorProduct.{u_1, u_3, u_4} R M ↥(eqLocus f g)
h :
  Eq (α := M ⊗[R] N)
    ((↑((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) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) x : M ⊗[R] N)
h_1 :
  Eq (α := M ⊗[R] N)
    ((↑((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)))
            y) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) y : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    ((↑((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 + y)) :
        M ⊗[R] N) :
      M ⊗[R] N)
    ((lTensor M (Submodule.subtype (eqLocus f g)) : (a : M ⊗[R] ↥(eqLocus f g)) → M ⊗[R] N) (x + y) : M ⊗[R] N)

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

Tactic:
simp [Module.Flat.ker_lTensor_eq]

Premises used: Module.Flat.ker_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 : 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))
rw :
  ((((AlgebraTensorModule.lTensor S M :
                (↥f.ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
              (a : ↥f.ker →ₗ[R] N) → M ⊗[R] ↥f.ker →ₗ[S] M ⊗[R] N)
            f.ker.subtype :
          TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
        (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      ((tensorKerInv 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)
⊢ (lTensor M f.ker.subtype : (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      ((tensorKerInv 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:
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 : 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))
⊢ ((((AlgebraTensorModule.lTensor S M :
                (↥f.ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
              (a : ↥f.ker →ₗ[R] N) → M ⊗[R] ↥f.ker →ₗ[S] M ⊗[R] N)
            f.ker.subtype :
          TensorProduct.{u_1, u_3, u_4} R M ↥f.ker →ₗ[S] M ⊗[R] N) :
        (a : M ⊗[R] ↥f.ker) → M ⊗[R] N)
      ((tensorKerInv 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:
simp [LinearMap.tensorKerInv]

Premises used: LinearMap.tensorKerInv