-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
M : Type u_4
inst_5 : AddCommGroup M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
N : Type u_5
inst_9 : AddCommGroup N
inst_10 : Module R N
inst_11 : Module B N
inst_12 : IsScalarTower R B N
n : Submodule B N
x : M
y : N
⊢ Eq (α :=
    HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
      (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
        (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
            (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
          ((↑R :
              {S : Type u_3} →
                {M M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_13 : Semiring S] →
                      [inst_14 : AddCommMonoid M] →
                        [inst_15 : AddCommMonoid M₂] →
                          [inst_16 : Module R M] →
                            [inst_17 : Module R M₂] →
                              [inst_18 : Module S M] →
                                [inst_19 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            n.subtype))))
    ((tensorQuotientEquiv A B M n :
          (a : M ⊗[R] (N ⧸ n)) →
            M ⊗[R] N ⧸
              ((lTensor A M : (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
                  ((↑R :
                      {S : Type u_3} →
                        {M M₂ : Type u_5} →
                          [inst : Semiring R] →
                            [inst_13 : Semiring S] →
                              [inst_14 : AddCommMonoid M] →
                                [inst_15 : AddCommMonoid M₂] →
                                  [inst_16 : Module R M] →
                                    [inst_17 : Module R M₂] →
                                      [inst_18 : Module S M] →
                                        [inst_19 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    n.subtype)).range)
        (x ⊗ₜ[R] Submodule.Quotient.mk y) :
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
        (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
          (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
              (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
            ((↑R :
                {S : Type u_3} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              n.subtype))))
    (Submodule.Quotient.mk (x ⊗ₜ[R] y) :
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule A (M ⊗[R] N))
        (LinearMap.range (R := A) (M := TensorProduct.{u_1, u_4, u_5} R M ↥n) (τ₁₂ := RingHom.id A)
          (((lTensor A M : (↥n →ₗ[R] N) →ₗ[R] TensorProduct.{u_1, u_4, u_5} R M ↥n →ₗ[A] M ⊗[R] N) :
              (a : ↥n →ₗ[R] N) → M ⊗[R] ↥n →ₗ[A] M ⊗[R] N)
            ((↑R :
                {S : Type u_3} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              n.subtype))))

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, Submodule.restrictScalars, LinearMap.range, TensorProduct.map, TensorProduct.tmul, Submodule.map, TensorProduct.lift, AddCon.toQuotient, TensorProduct.AlgebraTensorModule.map, rfl, Submodule.copy, TensorProduct.AlgebraTensorModule.lift