-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N1 : Type u_1
inst_3 : AddCommGroup N1
inst_4 : Module R N1
N2 : Type u_2
inst_5 : AddCommGroup N2
inst_6 : Module R N2
N3 : Type u_3
inst_7 : AddCommGroup N3
inst_8 : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex :
  Function.Exact (M := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
E : Submodule R N3 :=
  Submodule.span R (singleton (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3))
hE : Nontrivial.{u_3} ↥E
eq1 :
  ∀ (m : M),
    Eq (α := N3 ⊗[R] M) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) ⊗ₜ[R] m : N3 ⊗[R] M) (0 : N3 ⊗[R] M)
c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R
b : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → ↥E
a : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → M
hy : ∀ ⦃a_1 : TensorProduct.{u, u_3, v} R (↥E) M⦄ (a_2 : a_1 ∈ (↑c.support : Set (↥E ⊗[R] M))), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ c.support → R :=
  fun (a : TensorProduct.{u, u_3, v} R (↥E) M) (ha : a ∈ c.support) ↦
    ⋯.choose (p := fun (a_1 : R) ↦
      HSMul.hSMul (β := N3) a_1 ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) = (↑(b ha) : N3))
hr :
  ∀ ⦃i : TensorProduct.{u, u_3, v} R (↥E) M⦄ (hi : i ∈ c.support),
    b hi =
      HSMul.hSMul (β := ↥E) (r hi)
        (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ : ↥E)
i : TensorProduct.{u, u_3, v} R (↥E) M
hi : i ∈ c.support
h :
  Eq (α := N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
        (HSMul.hSMul (α := R) (β := TensorProduct.{u, u_3, v} R (↥E) M)
          ((c : (a : ↥E ⊗[R] M) → R) (b hi ⊗ₜ[R] a hi) : R) (b hi ⊗ₜ[R] a hi)) :
      N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0 : N3 ⊗[R] M)
h₁ :
  Eq (α := N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
        (HSMul.hSMul (α := R) (β := TensorProduct.{u, u_3, v} R (↥E) M)
          ((c : (a : ↥E ⊗[R] M) → R)
              (HSMul.hSMul (β := ↥E) (r hi)
                  (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ :
                    ↥E) ⊗ₜ[R]
                a hi) :
            R)
          (HSMul.hSMul (β := ↥E) (r hi)
              (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ :
                ↥E) ⊗ₜ[R]
            a hi)) :
      N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0 : N3 ⊗[R] M)
h₂ :
  Eq (α := N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
        (HSMul.hSMul (α := R) (β := TensorProduct.{u, u_3, v} R (↥E) M)
          ((c : (a : ↥E ⊗[R] M) → R)
              (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
                  (r hi • a hi) :
                TensorProduct.{u, u_3, v} R (↥E) M) :
            R)
          (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
              (r hi • a hi) :
            TensorProduct.{u, u_3, v} R (↥E) M)) :
      N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0 : N3 ⊗[R] M)
h₃ :
  HSMul.hSMul (α := R) (β := N3 ⊗[R] M)
      ((c : (a : ↥E ⊗[R] M) → R)
          (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
              (r hi • a hi) :
            TensorProduct.{u, u_3, v} R (↥E) M) :
        R)
      ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
          (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
            (r hi • a hi)) :
        N3 ⊗[R] M) =
    (LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0
h₄ :
  HSMul.hSMul (α := R) (β := N3 ⊗[R] M)
      ((c : (a : ↥E ⊗[R] M) → R)
          (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
              (r hi • a hi) :
            TensorProduct.{u, u_3, v} R (↥E) M) :
        R)
      ((E.subtype : (a : ↥E) → N3)
            (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ :
              ↥E) ⊗ₜ[R]
          (r hi • a hi) :
        N3 ⊗[R] M) =
    (LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0
h₅ :
  HSMul.hSMul (α := R) (β := N3 ⊗[R] M)
      ((c : (a : ↥E ⊗[R] M) → R)
          (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
              (r hi • a hi) :
            TensorProduct.{u, u_3, v} R (↥E) M) :
        R)
      ((↑(Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯) : N3) ⊗ₜ[R]
          (r hi • a hi) :
        N3 ⊗[R] M) =
    (LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0
h₆ :
  HSMul.hSMul (α := R) (β := N3 ⊗[R] M)
      ((c : (a : ↥E ⊗[R] M) → R)
          (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ ⊗ₜ[R]
              (r hi • a hi) :
            TensorProduct.{u, u_3, v} R (↥E) M) :
        R)
      0 =
    (LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0
h₇ : Eq (α := N3 ⊗[R] M) 0 ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0)
h₈ h₉ : Eq (α := N3 ⊗[R] M) 0 0
⊢ Eq (α := N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
        (HSMul.hSMul (α := R) ((c : (a : ↥E ⊗[R] M) → R) i : R) i) :
      N3 ⊗[R] M)
    ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0 : N3 ⊗[R] M)

Tactic:
rw [← hy hi, hr hi, smul_tmul, map_smul, LinearMap.rTensor_tmul, Submodule.subtype_apply, eq1,
      smul_zero, map_zero]

Premises used: TensorProduct.smul_tmul, LinearMap.rTensor_tmul, Submodule.subtype_apply, smul_zero, map_zero, map_smul