awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
H₅ :
  Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
H₆ :
  Injective (α := R ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] (P ⊗[R] Q))
    (⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) : (a : R ⊗[R] (P ⊗[R] Q)) → K ⊗[R] (P ⊗[R] Q))
⊢ Injective (α := P ⊗[R] Q) (β := R ⊗[R] (P ⊗[R] Q))
    (⇑(LinearEquiv.symm (TensorProduct.lid R (P ⊗[R] Q))) : (a : P ⊗[R] Q) → R ⊗[R] (P ⊗[R] Q))

Tactic:
have H₇ := (TensorProduct.lid R (P ⊗[R] Q)).symm.injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
H₅ :
  Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
H₆ :
  Injective (α := R ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] (P ⊗[R] Q))
    (⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) : (a : R ⊗[R] (P ⊗[R] Q)) → K ⊗[R] (P ⊗[R] Q))
H₇ :
  Injective (α := P ⊗[R] Q) (β := R ⊗[R] (P ⊗[R] Q))
    (⇑(LinearEquiv.symm (TensorProduct.lid R (P ⊗[R] Q))) : (a : P ⊗[R] Q) → R ⊗[R] (P ⊗[R] Q))
p : P
q : Q
⊢ Eq (α := K ⊗[R] (M ⊗[R] N)) (1 ⊗ₜ[R] ((f : (a : P) → M) p ⊗ₜ[R] (g : (a : Q) → N) q) : K ⊗[R] (M ⊗[R] N))
    (((AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
          (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
        (HSMul.hSMul (α := K) (β := K ⊗[R] M) 1
            ((algebraMap R K : (a : R) → K) 1 ⊗ₜ[R] (f : (a : P) → M) p : K ⊗[R] M) ⊗ₜ[R]
          (g : (a : Q) → N) q) :
      K ⊗[R] (M ⊗[R] N))

Tactic:
simp only [map_one, one_smul, AlgebraTensorModule.assoc_tmul]

Premises used: TensorProduct.AlgebraTensorModule.assoc_tmul, one_smul, map_one
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Injective (α := ι × κ →₀ R) (β := M ⊗[R] N)
    (Function.comp (β := (ι →₀ R) ⊗[R] (κ →₀ R))
      (⇑(TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) :
        (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → M ⊗[R] N)
      (⇑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)))

Tactic:
(TensorProduct.map_injective_of_flat_flat_of_isDomain _ _ hv hw).comp
      (finsuppTensorFinsupp' _ _ _).symm.injective

Premises used: LinearEquiv.symm, TensorProduct.map_injective_of_flat_flat_of_isDomain, Function.Injective.comp, finsuppTensorFinsupp', LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
h :
  Eq (α := (ι × κ →₀ R) → M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
    (Function.comp (β := (ι →₀ R) ⊗[R] (κ →₀ R))
      (⇑(TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) :
        (a : (ι →₀ R) ⊗[R] (κ →₀ R)) → M ⊗[R] N)
      (⇑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)))
⊢ Injective (α := ι × κ →₀ R) (β := M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)

Tactic:
convert!
    (TensorProduct.map_injective_of_flat_flat_of_isDomain _ _ hv hw).comp
      (finsuppTensorFinsupp' _ _ _).symm.injective

Premises used: LinearEquiv.symm, TensorProduct.map_injective_of_flat_flat_of_isDomain, Function.Injective.comp, finsuppTensorFinsupp', LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
h :
  Eq (α := (ι × κ →₀ R) →ₗ[R] M ⊗[R] N) (Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2)
    (TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
      (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R)))
⊢ Eq (α := (ι × κ →₀ R) → M ⊗[R] N)
    (⇑(Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) : (a : ι × κ →₀ R) → M ⊗[R] N)
    (⇑(TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
          (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R))) :
      (a : ι × κ →₀ R) → M ⊗[R] N)

Tactic:
congr!
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
hv : LinearIndependent R v
hw : LinearIndependent R w
i : ι × κ
⊢ Eq (α := M ⊗[R] N)
    (((Finsupp.linearCombination R fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) ∘ₗ Finsupp.lsingle i : (a : R) → M ⊗[R] N) 1)
    (((TensorProduct.map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ
            (↑(LinearEquiv.symm (finsuppTensorFinsupp' R ι κ)) : (ι × κ →₀ R) →ₗ[R] (ι →₀ R) ⊗[R] (κ →₀ R))) ∘ₗ
          Finsupp.lsingle i :
        (a : R) → M ⊗[R] N)
      1)

Tactic:
simp [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
s : Set ι
t : Set κ
hv : LinearIndepOn R v s
hw : LinearIndepOn R w t
⊢ LinearIndepOn R (M := M ⊗[R] N) (fun (i : ι × κ) ↦ v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)

Tactic:
((hv.tmul_of_isDomain hw).comp _ (Equiv.Set.prod _ _).injective :)

Premises used: LinearIndependent.tmul_of_isDomain, Equiv.Set.prod, Equiv.injective, TensorProduct.tmul, LinearIndependent.comp, LinearIndepOn
-- 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 : Flat R M
rw :
  Function.Exact (M := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) (N := M ⊗[R] N) (P := M ⊗[R] P)
    (⇑(((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)
    (⇑(((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) :
      (a : M ⊗[R] N) → M ⊗[R] P)
⊢ Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.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))
    (LinearMap.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))

Tactic:
rw [← LinearMap.exact_iff]

Premises used: LinearMap.exact_iff
-- 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 : Flat R M
⊢ Function.Exact (M := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) (N := M ⊗[R] N) (P := M ⊗[R] P)
    (⇑(((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)
    (⇑(((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) :
      (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
Module.Flat.lTensor_exact M (LinearMap.exact_subtype_ker_map f)

Premises used: Module.Flat.lTensor_exact, LinearMap.exact_subtype_ker_map, TensorProduct.tmul, AddCon.toQuotient
-- 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 : Flat R M
⊢ Function.Exact (M := TensorProduct.{u_1, u_3, u_4} R M ↥f.ker) (N := M ⊗[R] N) (P := M ⊗[R] P)
    (⇑(((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)
    (⇑(((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) :
      (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
exact Module.Flat.lTensor_exact M (LinearMap.exact_subtype_ker_map f)

Premises used: Module.Flat.lTensor_exact, LinearMap.exact_subtype_ker_map
-- 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 : Flat R M
rw :
  (HSub.hSub (α := M ⊗[R] N →ₗ[S] M ⊗[R] P) (β := 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)).ker =
    LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype)
⊢ Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.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))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(LinearMap.eqLocus f g)) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(LinearMap.eqLocus f g) →ₗ[R] N) →ₗ[R]
              TensorProduct.{u_1, u_3, u_4} R M ↥(LinearMap.eqLocus f g) →ₗ[S] M ⊗[R] N) :
          (a : ↥(LinearMap.eqLocus f g) →ₗ[R] N) → M ⊗[R] ↥(LinearMap.eqLocus f g) →ₗ[S] M ⊗[R] N)
        (Submodule.subtype (LinearMap.eqLocus f g))))

Tactic:
rw [LinearMap.eqLocus_eq_ker_sub, LinearMap.eqLocus_eq_ker_sub]

Premises used: LinearMap.eqLocus_eq_ker_sub
-- 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 : Flat R M
rw :
  Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.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 - g)))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype))
rw₁ rw₂ :
  Eq (α := Submodule S (M ⊗[R] N))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype))
    (LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype))
⊢ (HSub.hSub (α := M ⊗[R] N →ₗ[S] M ⊗[R] P) (β := 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)).ker =
    LinearMap.range (R := S) (M := TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker) (τ₁₂ := RingHom.id S)
      (((AlgebraTensorModule.lTensor S M :
            (↥(f - g).ker →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_3, u_4} R M ↥(f - g).ker →ₗ[S] M ⊗[R] N) :
          (a : ↥(f - g).ker →ₗ[R] N) → M ⊗[R] ↥(f - g).ker →ₗ[S] M ⊗[R] N)
        (f - g).ker.subtype)

Tactic:
rw [← map_sub, ker_lTensor_eq]

Premises used: Module.Flat.ker_lTensor_eq, map_sub
-- 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 : ↥(eqLocus f g)
⊢ 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))
    (m ⊗ₜ[R] (↑a : N))

Tactic:
simp [show f a = g a from a.property]

Premises used: Subtype.property
-- 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 : ↥(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] (↑(x + y) : N)) ⋯ =
    HAdd.hAdd (α :=
      ↥(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)))
      (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)) ⋯)
      (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] (↑y : N)) ⋯)

Tactic:
simp [tmul_add]

Premises used: TensorProduct.tmul_add