awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
f : TensorProduct.{u_1, u_2, u_3} R (↥m) N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : TensorProduct.{u_1, u_2, u_3} R M ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
hl :
  ∀ (x : ↥m) (y : N),
    Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      (((((AlgebraTensorModule.curry
                      (f.coprod g ∘ₗ
                        LinearMap.inl R (TensorProduct.{u_1, u_2, u_3} R (↥m) N)
                          (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                    ↥m →ₗ[R] N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                  (a : ↥m) → N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
                x :
              N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
            (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          y :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      (((((AlgebraTensorModule.curry
                      (0 ∘ₗ
                        LinearMap.inl R (TensorProduct.{u_1, u_2, u_3} R (↥m) N)
                          (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                    ↥m →ₗ[R] N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                  (a : ↥m) → N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
                x :
              N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
            (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          y :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
hr :
  ∀ (x : M) (y : ↥n),
    Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      (((((AlgebraTensorModule.curry
                      (f.coprod g ∘ₗ
                        LinearMap.inr R (TensorProduct.{u_1, u_2, u_3} R (↥m) N)
                          (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                    M →ₗ[R] ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                  (a : M) → ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
                x :
              ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
            (a : ↥n) → (M ⧸ m) ⊗[R] (N ⧸ n))
          y :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      (((((AlgebraTensorModule.curry
                      (0 ∘ₗ
                        LinearMap.inr R (TensorProduct.{u_1, u_2, u_3} R (↥m) N)
                          (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                    M →ₗ[R] ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                  (a : M) → ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
                x :
              ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
            (a : ↥n) → (M ⧸ m) ⊗[R] (N ⧸ n))
          y :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
⊢ f.coprod g = 0

Tactic:
ext x y
-- 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
f : TensorProduct.{u_1, u_2, u_3} R (↥m) N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : TensorProduct.{u_1, u_2, u_3} R M ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
x : ↥m
y : N
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (((((AlgebraTensorModule.curry
                    (f.coprod g ∘ₗ
                      LinearMap.inl R (TensorProduct.{u_1, u_2, u_3} R (↥m) N) (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                  ↥m →ₗ[R] N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : ↥m) → N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x :
            N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
          (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
        y :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (((((AlgebraTensorModule.curry
                    (0 ∘ₗ
                      LinearMap.inl R (TensorProduct.{u_1, u_2, u_3} R (↥m) N) (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                  ↥m →ₗ[R] N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : ↥m) → N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x :
            N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
          (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
        y :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))

Tactic:
simp [f, Submodule.Quotient.mk_eq_zero _ |>.2 x.2]

Premises used: Iff.mpr, Submodule.Quotient.mk_eq_zero, Subtype.property
-- 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
f : TensorProduct.{u_1, u_2, u_3} R (↥m) N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : TensorProduct.{u_1, u_2, u_3} R M ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
x : M
y : ↥n
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (((((AlgebraTensorModule.curry
                    (f.coprod g ∘ₗ
                      LinearMap.inr R (TensorProduct.{u_1, u_2, u_3} R (↥m) N) (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                  M →ₗ[R] ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : M) → ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x :
            ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
          (a : ↥n) → (M ⧸ m) ⊗[R] (N ⧸ n))
        y :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (((((AlgebraTensorModule.curry
                    (0 ∘ₗ
                      LinearMap.inr R (TensorProduct.{u_1, u_2, u_3} R (↥m) N) (TensorProduct.{u_1, u_2, u_3} R M ↥n)) :
                  M →ₗ[R] ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : M) → ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x :
            ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
          (a : ↥n) → (M ⧸ m) ⊗[R] (N ⧸ n))
        y :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))

Tactic:
simp [g, Submodule.Quotient.mk_eq_zero _ |>.2 y.2]

Premises used: Iff.mpr, Submodule.Quotient.mk_eq_zero, Subtype.property
-- 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
f : TensorProduct.{u_1, u_2, u_3} R (↥m) N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : TensorProduct.{u_1, u_2, u_3} R M ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
⊢ f.coprod g = 0

Tactic:
have eq : LinearMap.coprod f g = 0 := by
        ext x y
        · simp [f, Submodule.Quotient.mk_eq_zero _ |>.2 x.2]
        · simp [g, Submodule.Quotient.mk_eq_zero _ |>.2 y.2]
-- 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
f : TensorProduct.{u_1, u_2, u_3} R (↥m) N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : TensorProduct.{u_1, u_2, u_3} R M ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
eq : f.coprod g = 0
⊢ HAdd.hAdd (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) (β :=
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      ((map m.mkQ n.mkQ : (a : M ⊗[R] N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          ((map m.subtype LinearMap.id : (a : ↥m ⊗[R] N) → M ⊗[R] N) a) :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      ((map m.mkQ n.mkQ : (a : M ⊗[R] N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          ((map LinearMap.id n.subtype : (a : M ⊗[R] ↥n) → M ⊗[R] N) b) :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) =
    0

Tactic:
congr($eq (a, b))

Premises used: congrArg, id, Prod.mk, DFunLike.coe
-- 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
f : TensorProduct.{u_1, u_2, u_3} R (↥m) N →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : TensorProduct.{u_1, u_2, u_3} R M ↥n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) :=
  map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
eq : f.coprod g = 0
⊢ HAdd.hAdd (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) (β :=
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      ((map m.mkQ n.mkQ : (a : M ⊗[R] N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          ((map m.subtype LinearMap.id : (a : ↥m ⊗[R] N) → M ⊗[R] N) a) :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      ((map m.mkQ n.mkQ : (a : M ⊗[R] N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          ((map LinearMap.id n.subtype : (a : M ⊗[R] ↥n) → M ⊗[R] N) b) :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) =
    0

Tactic:
exact congr($eq (a, b))
-- 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
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))

Tactic:
simp
-- 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
a :
  ∀ (x : M ⧸ m) (x_1 : N),
    Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      ((((AlgebraTensorModule.curry
                      ((LinearMap.range (map m.subtype LinearMap.id) ⊔
                              LinearMap.range (map LinearMap.id n.subtype)).liftQ
                          (map m.mkQ n.mkQ) ⋯ ∘ₗ
                        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)
                                ⋯))
                            ⋯)) :
                    M ⧸ m →ₗ[R] N ⧸ n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                  (a : M ⧸ m) → N ⧸ n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
                x ∘ₗ
              n.mkQ :
            (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          x_1 :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
      ((((AlgebraTensorModule.curry LinearMap.id :
                    M ⧸ m →ₗ[R] N ⧸ n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                  (a : M ⧸ m) → N ⧸ n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
                x ∘ₗ
              n.mkQ :
            (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
          x_1 :
        TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n) →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    ((LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).liftQ
        (map m.mkQ n.mkQ) ⋯ ∘ₗ
      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.id

Tactic:
ext
-- 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
x : M ⧸ m
x_1 : N
a :
  Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (((LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).liftQ
            (map m.mkQ n.mkQ) ⋯ :
          (a : M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) →
            (M ⧸ m) ⊗[R] (N ⧸ n))
        ((((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)
                        ⋯))
                    ⋯ :
                  (a : M ⧸ m) →
                    N ⧸ n →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
                x :
              N ⧸ n →ₗ[R]
                M ⊗[R] N ⧸
                  LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
            (a : N ⧸ n) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
          (Submodule.Quotient.mk x_1)) :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (x ⊗ₜ[R] Submodule.Quotient.mk x_1 : TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    ((((AlgebraTensorModule.curry
                    ((LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).liftQ
                        (map m.mkQ n.mkQ) ⋯ ∘ₗ
                      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)
                              ⋯))
                          ⋯)) :
                  M ⧸ m →ₗ[R] N ⧸ n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : M ⧸ m) → N ⧸ n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x ∘ₗ
            n.mkQ :
          (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
        x_1 :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    ((((AlgebraTensorModule.curry LinearMap.id :
                  M ⧸ m →ₗ[R] N ⧸ n →ₗ[R] TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) :
                (a : M ⧸ m) → N ⧸ n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n))
              x ∘ₗ
            n.mkQ :
          (a : N) → (M ⧸ m) ⊗[R] (N ⧸ n))
        x_1 :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))

Tactic:
simp
-- 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
x : M
y : N
⊢ Eq (α := M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    ((quotientTensorQuotientEquiv m n :
          (a : (M ⧸ m) ⊗[R] (N ⧸ n)) →
            M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
        (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y) :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    (Submodule.Quotient.mk (x ⊗ₜ[R] y) :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, setOf, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- 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
x : M
y : N
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (((quotientTensorQuotientEquiv m n).symm :
          (a : M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) →
            (M ⧸ m) ⊗[R] (N ⧸ n))
        (Submodule.Quotient.mk (x ⊗ₜ[R] y)) :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))
    (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y : TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- 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
⊢ Eq (α := Submodule R (M ⊗[R] N))
    (Submodule.map (↑(LinearEquiv.refl R (M ⊗[R] N)) : M ⊗[R] N →ₗ[R] M ⊗[R] N)
      (LinearMap.range (map m.subtype LinearMap.id) ⊔
        LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R M ↥⊥) (map LinearMap.id (Submodule.subtype ⊥))))
    (LinearMap.range (map m.subtype LinearMap.id))

Tactic:
simp [Submodule.map_span, range_map_eq_span_tmul]

Premises used: TensorProduct.range_map_eq_span_tmul, Submodule.map_span
-- 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
x : M
y : N
⊢ Eq (α := HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N)) (LinearMap.range (map m.subtype LinearMap.id)))
    ((quotientTensorEquiv N m : (a : (M ⧸ m) ⊗[R] N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range)
        (Submodule.Quotient.mk x ⊗ₜ[R] y) :
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N)) (LinearMap.range (map m.subtype LinearMap.id)))
    (Submodule.Quotient.mk (x ⊗ₜ[R] y) :
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N)) (LinearMap.range (map m.subtype LinearMap.id)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, TensorProduct.tmul, AddCon.toQuotient, rfl
-- 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
x : M
y : N
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) N)
    ((LinearEquiv.symm (quotientTensorEquiv N m) : (a : M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range) → (M ⧸ m) ⊗[R] N)
        (Submodule.Quotient.mk (x ⊗ₜ[R] y)) :
      TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) N)
    (Submodule.Quotient.mk x ⊗ₜ[R] y : TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- 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
n : Submodule R N
⊢ Eq (α := Submodule R (M ⊗[R] N))
    (Submodule.map (↑(LinearEquiv.refl R (M ⊗[R] N)) : M ⊗[R] N →ₗ[R] M ⊗[R] N)
      (LinearMap.range (M := TensorProduct.{u_1, u_2, u_3} R (↥⊥) N) (map (Submodule.subtype ⊥) LinearMap.id) ⊔
        LinearMap.range (map LinearMap.id n.subtype)))
    (LinearMap.range (map LinearMap.id n.subtype))

Tactic:
simp [range_map_eq_span_tmul]

Premises used: TensorProduct.range_map_eq_span_tmul
-- 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
n : Submodule R N
x : M
y : N
⊢ Eq (α := HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N)) (LinearMap.range (map LinearMap.id n.subtype)))
    ((tensorQuotientEquiv M n : (a : M ⊗[R] (N ⧸ n)) → M ⊗[R] N ⧸ (map LinearMap.id n.subtype).range)
        (x ⊗ₜ[R] Submodule.Quotient.mk y) :
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N)) (LinearMap.range (map LinearMap.id n.subtype)))
    (Submodule.Quotient.mk (x ⊗ₜ[R] y) :
      HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N)) (LinearMap.range (map LinearMap.id n.subtype)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, TensorProduct.tmul, AddCon.toQuotient, rfl