awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
x : M₁
x_1 : M₂
⊢ Eq (α := M₁ ⊗[R] (M₂ × M₃))
    ((((AlgebraTensorModule.curry
                    (LinearMap.coprod
                        (((AlgebraTensorModule.lTensor S M₁ :
                              (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                            (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                          (LinearMap.inl R M₂ M₃))
                        (((AlgebraTensorModule.lTensor S M₁ :
                              (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                            (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                          (LinearMap.inr R M₂ M₃)) ∘ₗ
                      AlgebraTensorModule.lift
                        (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                          LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃))) :
                  M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
              x ∘ₗ
            LinearMap.inl R M₂ M₃ :
          (a : M₂) → M₁ ⊗[R] (M₂ × M₃))
        x_1 :
      M₁ ⊗[R] (M₂ × M₃))
    ((((AlgebraTensorModule.curry LinearMap.id : M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
              x ∘ₗ
            LinearMap.inl R M₂ M₃ :
          (a : M₂) → M₁ ⊗[R] (M₂ × M₃))
        x_1 :
      M₁ ⊗[R] (M₂ × M₃))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
x : M₁
x_1 : M₃
⊢ Eq (α := M₁ ⊗[R] (M₂ × M₃))
    ((((AlgebraTensorModule.curry
                    (LinearMap.coprod
                        (((AlgebraTensorModule.lTensor S M₁ :
                              (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                            (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                          (LinearMap.inl R M₂ M₃))
                        (((AlgebraTensorModule.lTensor S M₁ :
                              (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                            (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                          (LinearMap.inr R M₂ M₃)) ∘ₗ
                      AlgebraTensorModule.lift
                        (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                          LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃))) :
                  M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
              x ∘ₗ
            LinearMap.inr R M₂ M₃ :
          (a : M₃) → M₁ ⊗[R] (M₂ × M₃))
        x_1 :
      M₁ ⊗[R] (M₂ × M₃))
    ((((AlgebraTensorModule.curry LinearMap.id : M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
              x ∘ₗ
            LinearMap.inr R M₂ M₃ :
          (a : M₃) → M₁ ⊗[R] (M₂ × M₃))
        x_1 :
      M₁ ⊗[R] (M₂ × M₃))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
m₁ : M₁
m : M₂ × M₃
⊢ Eq (α := M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
    (((prodRight R S M₁ M₂ M₃ : M₁ ⊗[R] (M₂ × M₃) ≃ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₁ ⊗[R] (M₂ × M₃)) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        (m₁ ⊗ₜ[R] m) :
      M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
    ((m₁ ⊗ₜ[R] m.1, m₁ ⊗ₜ[R] m.2) : M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Function.prod, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
m₁ : M₁
m₂ : M₂
m₃ : M₃
⊢ Eq (α := M₁ ⊗[R] (M₂ × M₃))
    (((LinearEquiv.symm (prodRight R S M₁ M₂ M₃) : (M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ≃ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
          (a : M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) → M₁ ⊗[R] (M₂ × M₃))
        (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) :
      M₁ ⊗[R] (M₂ × M₃))
    (m₁ ⊗ₜ[R] (m₂, m₃) : M₁ ⊗[R] (M₂ × M₃))

Tactic:
(LinearEquiv.symm_apply_eq _).mpr rfl

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module S M₂
inst_12 : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ (LinearEquiv.toAddEquiv
          ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
              (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
            (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
              (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
        (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
      (HSMul.hSMul (β := (M₁ × M₂) ⊗[R] M₃) c 0) =
    HSMul.hSMul (β := M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) c
      ((LinearEquiv.toAddEquiv
            ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
              (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
          (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
        0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module S M₂
inst_12 : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ ∀ (x : M₁ × M₂) (y : M₃),
    (LinearEquiv.toAddEquiv
            ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
              (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
          (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
        (HSMul.hSMul (β := (M₁ × M₂) ⊗[R] M₃) c (x ⊗ₜ[R] y)) =
      HSMul.hSMul (β := M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) c
        ((LinearEquiv.toAddEquiv
                ((TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ :
                    (M₁ × M₂) ⊗[R] M₃ ≃ₗ[R] M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≪≫ₗ
                  (LinearEquiv.prodCongr (TensorProduct.comm R M₃ M₁) (TensorProduct.comm R M₃ M₂) :
                    (M₃ ⊗[R] M₁ × M₃ ⊗[R] M₂) ≃ₗ[R] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)) :
              (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
            (x ⊗ₜ[R] y) :
          M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)

Tactic:
simp [TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module S M₂
inst_12 : IsScalarTower R S M₂
m₁ : M₁
m₂ : M₂
m₃ : M₃
⊢ Eq (α := M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
    (((prodLeft R S M₁ M₂ M₃ : (M₁ × M₂) ⊗[R] M₃ ≃ₗ[S] M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) :
          (a : (M₁ × M₂) ⊗[R] M₃) → M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
        ((m₁, m₂) ⊗ₜ[R] m₃) :
      M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)
    ((m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) : M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Prod.map, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module S M₂
inst_12 : IsScalarTower R S M₂
m₁ : M₁
m₂ : M₂
m₃ : M₃
⊢ Eq (α := (M₁ × M₂) ⊗[R] M₃)
    (((LinearEquiv.symm (prodLeft R S M₁ M₂ M₃) : (M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) ≃ₗ[S] (M₁ × M₂) ⊗[R] M₃) :
          (a : M₁ ⊗[R] M₃ × M₂ ⊗[R] M₃) → (M₁ × M₂) ⊗[R] M₃)
        (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) :
      (M₁ × M₂) ⊗[R] M₃)
    ((m₁, m₂) ⊗ₜ[R] m₃ : (M₁ × M₂) ⊗[R] M₃)

Tactic:
(LinearEquiv.symm_apply_eq _).mpr rfl

Premises used: Iff.mpr, LinearEquiv.symm_apply_eq, 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 : N
hx : x ∈ n
h :
  ∀ (y : M),
    Eq (α := M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
      ((((LinearMap.compr₂ (LinearMap.flip (mk R M N))
                    (LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).mkQ :
                  (a : N) → M →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
                x :
              M →ₗ[R]
                M ⊗[R] N ⧸
                  LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
            (a : M) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
          y :
        M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
      ((0 : (a : M) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) y :
        M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
⊢ Membership.mem (γ := Submodule R N)
    (LinearMap.ker (R₂ := R) (M₂ :=
      M →ₗ[R] M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
      (τ₁₂ := RingHom.id R)
      (LinearMap.compr₂ (LinearMap.flip (mk R M N))
        (LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).mkQ))
    x

Tactic:
ext 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
x : N
hx : x ∈ n
y : M
h : y ⊗ₜ[R] x ∈ 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))
    ((((LinearMap.compr₂ (LinearMap.flip (mk R M N))
                  (LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)).mkQ :
                (a : N) → M →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
              x :
            M →ₗ[R]
              M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
          (a : M) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
        y :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    ((0 : (a : M) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) y :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))

Tactic:
simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply,
        LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]

Premises used: LinearMap.zero_apply, TensorProduct.mk_apply, LinearMap.compr₂_apply, Submodule.mkQ_apply, LinearMap.flip_apply, Submodule.Quotient.mk_eq_zero
-- 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 : N
hx : x ∈ n
y : M
⊢ y ⊗ₜ[R] x ∈ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)

Tactic:
Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩

Premises used: Set.Mem, Subtype.mk, Exists.intro, TensorProduct.tmul, Submodule.mem_sup_right, 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 : N
hx : x ∈ n
y : M
⊢ y ⊗ₜ[R] x ∈ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)

Tactic:
exact Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, 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
hx : x ∈ m
h :
  ∀ (y : N),
    Eq (α := M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
      ((((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 →ₗ[R]
                      N ⧸ n →ₗ[R]
                        M ⊗[R] N ⧸
                          LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
                  (a : M) →
                    N ⧸ n →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
                x ∘ₗ
              n.mkQ :
            (a : N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
          y :
        M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
      ((0 ∘ₗ n.mkQ : (a : N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) y :
        M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
⊢ Membership.mem (γ := Submodule R M)
    (LinearMap.ker (R₂ := R) (M₂ :=
      N ⧸ n →ₗ[R]
        M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
      (τ₁₂ := RingHom.id R)
      (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 →ₗ[R]
          N ⧸ n →ₗ[R]
            M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)))
    x

Tactic:
ext 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
x : M
hx : x ∈ m
y : N
h : x ⊗ₜ[R] y ∈ 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))
    ((((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 →ₗ[R]
                    N ⧸ n →ₗ[R]
                      M ⊗[R] N ⧸
                        LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)) :
                (a : M) →
                  N ⧸ n →ₗ[R] M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
              x ∘ₗ
            n.mkQ :
          (a : N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range)
        y :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))
    ((0 ∘ₗ n.mkQ : (a : N) → M ⊗[R] N ⧸ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) y :
      M ⊗[R] N ⧸ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype))

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply,
        Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp,
        LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]

Premises used: LinearMap.zero_apply, TensorProduct.mk_apply, LinearMap.compr₂_apply, Submodule.mkQ_apply, LinearMap.flip_apply, Submodule.liftQ_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.zero_comp, Submodule.Quotient.mk_eq_zero
-- 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
hx : x ∈ m
y : N
⊢ x ⊗ₜ[R] y ∈ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)

Tactic:
Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩

Premises used: Set.Mem, Subtype.mk, Exists.intro, TensorProduct.tmul, Submodule.mem_sup_left, 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
hx : x ∈ m
y : N
⊢ x ⊗ₜ[R] y ∈ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)

Tactic:
exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, 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 ⊗[R] N
hx : x ∈ LinearMap.range (map m.subtype LinearMap.id) ⊔ LinearMap.range (map LinearMap.id n.subtype)
⊢ ∃ (y : M ⊗[R] N),
    Membership.mem (γ := Submodule R (M ⊗[R] N)) (LinearMap.range (map m.subtype LinearMap.id)) y ∧
      ∃ (z : M ⊗[R] N),
        Membership.mem (γ := Submodule R (M ⊗[R] N)) (LinearMap.range (map LinearMap.id n.subtype)) z ∧ y + z = x

Tactic:
rw [Submodule.mem_sup] at hx

Premises used: Submodule.mem_sup
-- 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 ⊗[R] N
hx :
  ∃ (y : M ⊗[R] N),
    Membership.mem (γ := Submodule R (M ⊗[R] N)) (LinearMap.range (map m.subtype LinearMap.id)) y ∧
      ∃ (z : M ⊗[R] N),
        Membership.mem (γ := Submodule R (M ⊗[R] N)) (LinearMap.range (map LinearMap.id n.subtype)) z ∧ y + z = x
rcases :
  ∀ (a : TensorProduct.{u_1, u_2, u_3} R (↥m) N) (b : TensorProduct.{u_1, u_2, u_3} R M ↥n),
    Membership.mem (γ := Submodule R (M ⊗[R] N))
      (LinearMap.ker (R₂ := R) (M₂ := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) (τ₁₂ := RingHom.id R)
        (map m.mkQ n.mkQ))
      (HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N)
        ((map m.subtype LinearMap.id : (a : ↥m ⊗[R] N) → M ⊗[R] N) a : M ⊗[R] N)
        ((map LinearMap.id n.subtype : (a : M ⊗[R] ↥n) → M ⊗[R] N) b : M ⊗[R] N))
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N))
    (LinearMap.ker (R₂ := R) (M₂ := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) (τ₁₂ := RingHom.id R)
      (map m.mkQ n.mkQ))
    x

Tactic:
rcases hx with ⟨_, ⟨a, rfl⟩, _, ⟨b, rfl⟩, rfl⟩

Premises used: 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
a : TensorProduct.{u_1, u_2, u_3} R (↥m) N
b : TensorProduct.{u_1, u_2, u_3} R M ↥n
simp :
  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
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N))
    (LinearMap.ker (R₂ := R) (M₂ := TensorProduct.{u_1, u_2, u_3} R (M ⧸ m) (N ⧸ n)) (τ₁₂ := RingHom.id R)
      (map m.mkQ n.mkQ))
    (HAdd.hAdd (α := M ⊗[R] N) (β := M ⊗[R] N) ((map m.subtype LinearMap.id : (a : ↥m ⊗[R] N) → M ⊗[R] N) a : M ⊗[R] N)
      ((map LinearMap.id n.subtype : (a : M ⊗[R] ↥n) → M ⊗[R] N) b : M ⊗[R] N))

Tactic:
simp only [LinearMap.mem_ker, map_add]

Premises used: map_add, LinearMap.mem_ker