-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ 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)
have 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)) sorry :
                  ↥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)) sorry :
              ↥E) ⊗ₜ[R]
          a hi)) :
    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]