-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  HasQuotient.Quotient (TensorProduct.{u, u_2, v} R (↥l23.ker) M) (B :=
    Submodule R (TensorProduct.{u, u_2, v} R (↥l23.ker) M))
    (LinearMap.range (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)) :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
y : N1 ⊗[R] M
hy : Eq (α := N2 ⊗[R] M) ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M) (x ⊗ₜ[R] m : N2 ⊗[R] M)
tmul :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype ∘ₗ
            TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
          (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → N2 ⊗[R] M)
        ((LinearMap.rTensor M
              (LinearMap.codRestrict (Submodule.inclusion complex).range
                (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
            (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
          y) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
tmul₁ :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype ∘ₗ LinearMap.rTensor M (Submodule.inclusion complex).range.subtype :
          (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → N2 ⊗[R] M)
        ((LinearMap.rTensor M
              (LinearMap.codRestrict (Submodule.inclusion complex).range
                (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
            (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
          y) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
tmul₂ :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M (l23.ker.subtype ∘ₗ (Submodule.inclusion complex).range.subtype) :
          (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → N2 ⊗[R] M)
        ((LinearMap.rTensor M
              (LinearMap.codRestrict (Submodule.inclusion complex).range
                (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
            (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
          y) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
tmul₃ :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M (l23.ker.subtype ∘ₗ (Submodule.inclusion complex).range.subtype) ∘ₗ
            LinearMap.rTensor M
              (LinearMap.codRestrict (Submodule.inclusion complex).range
                (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
          (a : N1 ⊗[R] M) → N2 ⊗[R] M)
        y :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
tmul₄ :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M
            ((l23.ker.subtype ∘ₗ (Submodule.inclusion complex).range.subtype) ∘ₗ
              LinearMap.codRestrict (Submodule.inclusion complex).range
                (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
          (a : N1 ⊗[R] M) → N2 ⊗[R] M)
        y :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
tmul₅ :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M
            (l23.ker.subtype ∘ₗ
              (Submodule.inclusion complex).range.subtype ∘ₗ
                LinearMap.codRestrict (Submodule.inclusion complex).range
                  (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
          (a : N1 ⊗[R] M) → N2 ⊗[R] M)
        y :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
tmul₆ :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M (l23.ker.subtype ∘ₗ Submodule.inclusion complex ∘ₗ l12.rangeRestrict) :
          (a : N1 ⊗[R] M) → N2 ⊗[R] M)
        y :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
⊢ Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype : (a : ↥l23.ker ⊗[R] M) → N2 ⊗[R] M)
        ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          ((LinearMap.rTensor M
                (LinearMap.codRestrict (Submodule.inclusion complex).range
                  (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
              (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
            y)) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
have tmul₇ : Eq (α := N2 ⊗[R] M)
  ((LinearMap.rTensor M ((l23.ker.subtype ∘ₗ Submodule.inclusion complex) ∘ₗ l12.rangeRestrict) :
        (a : N1 ⊗[R] M) → N2 ⊗[R] M)
      y :
    N2 ⊗[R] M)
  ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
Tactic: rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]