-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
m : Submodule R M
n : Submodule R N
⊢ Eq (α :=
    M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype) →ₗ[R]
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    (lift
        (m.liftQ
          (LinearMap.flip
            (n.liftQ
              (LinearMap.compr₂ (LinearMap.flip (mk R M N))
                (LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).mkQ)
              ⋯))
          ⋯) ∘ₗ
      (LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).liftQ
        (map m.mkQ n.mkQ) ⋯)
    LinearMap.id
have h : ∀ (x : M) (x_1 : N),
  Eq (α := M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    (((((AlgebraTensorModule.curry
                    ((lift
                          (m.liftQ
                            (LinearMap.flip
                              (n.liftQ
                                (LinearMap.compr₂ (LinearMap.flip (mk R M N))
                                  (LinearMap.range (map m.subtype LinearMap.id) ⊔
                                      LinearMap.range (map LinearMap.id n.subtype)).mkQ)
                                sorry))
                            sorry) ∘ₗ
                        (LinearMap.range (map m.subtype LinearMap.id) ⊔
                              LinearMap.range (map LinearMap.id n.subtype)).liftQ
                          (map m.mkQ n.mkQ) sorry) ∘ₗ
                      (LinearMap.range (map m.subtype LinearMap.id) ⊔
                          LinearMap.range (map LinearMap.id n.subtype)).mkQ) :
                  M →ₗ[R]
                    N →ₗ[R]
                      M ⊗[R] N ⧸
                        LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
                (a : M) → N →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
              x :
            N →ₗ[R]
              M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
          (a : N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
        x_1 :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    (((((AlgebraTensorModule.curry
                    (LinearMap.id ∘ₗ
                      (LinearMap.range (map m.subtype LinearMap.id) ⊔
                          LinearMap.range (map LinearMap.id n.subtype)).mkQ) :
                  M →ₗ[R]
                    N →ₗ[R]
                      M ⊗[R] N ⧸
                        LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
                (a : M) → N →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
              x :
            N →ₗ[R]
              M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
          (a : N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
        x_1 :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
Tactic: ext