awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Prod (goal)
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₃
⊢ Eq (α := M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
    (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₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
    (LinearMap.id : M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
have a : ∀ (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: ext
-- 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
x : N
hx : x ∈ n
⊢ 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
have 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))
Tactic: ext y
-- 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
x : N
hx : x ∈ n
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))
have h : y ⊗ₜ[R] x ∈ 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]
-- 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
x : M
hx : x ∈ m
⊢ 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
have 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)
                      sorry) :
                  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: ext y
-- 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
x : M
hx : x ∈ m
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))
have h : x ⊗ₜ[R] y ∈ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (hypothesis)
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)
⊢ 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
have 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
Tactic: rw [Submodule.mem_sup] at hx
Cleared hypotheses: hx
-- 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
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
⊢ 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
have 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))
Tactic: rcases hx with ⟨_, ⟨a, rfl⟩, _, ⟨b, rfl⟩, rfl⟩
Cleared hypotheses: x, hx
-- 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
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))
have 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
Tactic: simp only [LinearMap.mem_ker, map_add]
-- 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
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
have 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))
Tactic: ext x y
-- 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
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))
⊢ f.coprod g = 0
have 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))
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Quotient (hypothesis)
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
⊢ 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
have eq : 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]
-- 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 (α := 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
have 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) sorry ∘ₗ
                      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)) :
                  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: ext