-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
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
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)
                                  ⋯))
                              ⋯) ∘ₗ
                          (LinearMap.range (map m.subtype LinearMap.id) ⊔
                                LinearMap.range (map LinearMap.id n.subtype)).liftQ
                            (map m.mkQ n.mkQ) ⋯) ∘ₗ
                        (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))
⊢ 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

Tactic:
ext