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
n : Submodule R N
x : M
y : N
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R M (N ⧸ n))
    ((LinearEquiv.symm (tensorQuotientEquiv M n) : (a : M ⊗[R] N ⧸ (map LinearMap.id n.subtype).range) → M ⊗[R] (N ⧸ n))
        (Submodule.Quotient.mk (x ⊗ₜ[R] y)) :
      TensorProduct.{u_1, u_2, u_3} R M (N ⧸ n))
    (x ⊗ₜ[R] Submodule.Quotient.mk y : TensorProduct.{u_1, u_2, u_3} R 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
I : Ideal R
rw :
  Eq (α := Submodule R M)
    (LinearMap.range (M := TensorProduct.{u_1, u_1, u_2} R ↥I ↥⊤)
      (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        (↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv) : ↥I ⊗[R] ↥⊤ →ₗ[R] ↥I ⊗[R] M)))
    (LinearMap.range (M := TensorProduct.{u_1, u_1, u_2} R ↥I ↥⊤) (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤))
⊢ Submodule.map (M := R ⊗[R] M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)
      (LinearMap.range (map (Submodule.subtype I) LinearMap.id)) =
    HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
rw [← LinearMap.range_comp, ← (Submodule.topEquiv.lTensor I).range_comp, Submodule.smul_eq_map₂,
      map₂_eq_range_lift_comp_mapIncl]

Premises used: Submodule.smul_eq_map₂, Submodule.topEquiv, LinearEquiv.range_comp, TensorProduct.map₂_eq_range_lift_comp_mapIncl, LinearMap.range_comp, Membership.mem, Subtype, LinearEquiv.lTensor
-- 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
I : Ideal R
x : ↥I
x_1 : ↥⊤
⊢ Eq.{u_2 + 1} (α := M)
    ((((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
            (↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv) : ↥I ⊗[R] ↥⊤ →ₗ[R] ↥I ⊗[R] M) :
          (a : ↥I ⊗[R] ↥⊤) → M)
        (x ⊗ₜ[R] x_1) :
      M)
    ((lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤ : (a : ↥I ⊗[R] ↥⊤) → M) (x ⊗ₜ[R] x_1) : M)

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
I : Ideal R
⊢ Eq (α := Submodule R M)
    (LinearMap.range (M := TensorProduct.{u_1, u_1, u_2} R ↥I ↥⊤)
      (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        (↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv) : ↥I ⊗[R] ↥⊤ →ₗ[R] ↥I ⊗[R] M)))
    (LinearMap.range (M := TensorProduct.{u_1, u_1, u_2} R ↥I ↥⊤) (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤))

Tactic:
exact congr_arg _ (TensorProduct.ext' fun _ _ ↦ by simp)

Premises used: congr_arg, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
r : R
x : M
⊢ Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((quotTensorEquivQuotSMul M I : (a : (R ⧸ I) ⊗[R] M) → M ⧸ I • ⊤)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) r ⊗ₜ[R] x) :
      M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    (Submodule.Quotient.mk (r • x) : M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
(quotTensorEquivQuotSMul M I).eq_symm_apply.mp <|
    Eq.trans (congrArg (· ⊗ₜ[R] x) <|
        Eq.trans (congrArg (Ideal.Quotient.mk I)
                    (Eq.trans (smul_eq_mul ..) (mul_one r))).symm <|
          Submodule.Quotient.mk_smul I r 1) <|
      smul_tmul r _ x

Premises used: TensorProduct.smul_tmul, TensorProduct.quotTensorEquivQuotSMul, congrArg, Ideal.Quotient.mk, LinearEquiv.eq_symm_apply, Submodule.Quotient.mk_smul, Iff.mp, TensorProduct.tmul, smul_eq_mul, mul_one, OfNat.ofNat, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
x : M
rw :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) (Submodule.Quotient.mk (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x))
    (Submodule.Quotient.mk x)
⊢ Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((quotTensorEquivQuotSMul M I : (a : (R ⧸ I) ⊗[R] M) → M ⧸ I • ⊤) (1 ⊗ₜ[R] x) :
      M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    (Submodule.Quotient.mk x : M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
rw [← RingHom.map_one (Ideal.Quotient.mk I), TensorProduct.quotTensorEquivQuotSMul_mk_tmul]

Premises used: Ideal.Quotient.mk, RingHom.map_one, TensorProduct.quotTensorEquivQuotSMul_mk_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
x : M
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤) (Submodule.Quotient.mk (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x))
    (Submodule.Quotient.mk x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ (↑(quotTensorEquivQuotSMul M I) : (R ⧸ I) ⊗[R] M →ₗ[R] M ⧸ I • ⊤) ∘ₗ LinearMap.rTensor M (Submodule.mkQ I) =
    (HSMul.hSMul (β := Submodule R M) I ⊤).mkQ ∘ₗ (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)

Tactic:
TensorProduct.ext' (quotTensorEquivQuotSMul_mk_tmul I)

Premises used: TensorProduct.ext', TensorProduct.quotTensorEquivQuotSMul_mk_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
x : M
⊢ Eq (α := (R ⧸ I) ⊗[R] M)
    ((LinearEquiv.symm (quotTensorEquivQuotSMul M I) : (a : M ⧸ I • ⊤) → (R ⧸ I) ⊗[R] M) (Submodule.Quotient.mk x) :
      (R ⧸ I) ⊗[R] M)
    (1 ⊗ₜ[R] x : (R ⧸ I) ⊗[R] M)

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
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ (↑(LinearEquiv.symm (quotTensorEquivQuotSMul M I)) : M ⧸ I • ⊤ →ₗ[R] (R ⧸ I) ⊗[R] M) ∘ₗ
      (HSMul.hSMul (β := Submodule R M) I ⊤).mkQ =
    (mk R (R ⧸ I) M : (a : R ⧸ I) → M →ₗ[R] (R ⧸ I) ⊗[R] M) 1

Tactic:
LinearMap.ext (quotTensorEquivQuotSMul_symm_mk I)

Premises used: LinearMap.ext, TensorProduct.quotTensorEquivQuotSMul_symm_mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ (↑(quotTensorEquivQuotSMul M I) : (R ⧸ I) ⊗[R] M →ₗ[R] M ⧸ I • ⊤) ∘ₗ
      (mk R (R ⧸ I) M : (a : R ⧸ I) → M →ₗ[R] (R ⧸ I) ⊗[R] M) 1 =
    (HSMul.hSMul (β := Submodule R M) I ⊤).mkQ

Tactic:
Eq.symm <| (LinearEquiv.toLinearMap_symm_comp_eq _ _).mp <|
    quotTensorEquivQuotSMul_symm_comp_mkQ I

Premises used: LinearEquiv.toLinearMap_symm_comp_eq, Iff.mp, Eq.symm, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
x : M
r : R
⊢ Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    ((tensorQuotEquivQuotSMul M I : (a : M ⊗[R] (R ⧸ I)) → M ⧸ I • ⊤)
        (x ⊗ₜ[R] (Ideal.Quotient.mk I : (a : R) → R ⧸ I) r) :
      M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
    (Submodule.Quotient.mk (r • x) : M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
quotTensorEquivQuotSMul_mk_tmul I r x

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, TensorProduct.quotTensorEquivQuotSMul_mk_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ (↑(tensorQuotEquivQuotSMul M I) : M ⊗[R] (R ⧸ I) →ₗ[R] M ⧸ I • ⊤) ∘ₗ LinearMap.lTensor M (Submodule.mkQ I) =
    (HSMul.hSMul (β := Submodule R M) I ⊤).mkQ ∘ₗ (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M)

Tactic:
TensorProduct.ext' (tensorQuotEquivQuotSMul_tmul_mk I)

Premises used: TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
x : M
⊢ Eq (α := M ⊗[R] (R ⧸ I))
    ((LinearEquiv.symm (tensorQuotEquivQuotSMul M I) : (a : M ⧸ I • ⊤) → M ⊗[R] (R ⧸ I)) (Submodule.Quotient.mk x) :
      M ⊗[R] (R ⧸ I))
    (x ⊗ₜ[R] 1 : M ⊗[R] (R ⧸ I))

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
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ (↑(LinearEquiv.symm (tensorQuotEquivQuotSMul M I)) : M ⧸ I • ⊤ →ₗ[R] M ⊗[R] (R ⧸ I)) ∘ₗ
      (HSMul.hSMul (β := Submodule R M) I ⊤).mkQ =
    (LinearMap.flip (mk R M (R ⧸ I)) : (a : R ⧸ I) → M →ₗ[R] M ⊗[R] (R ⧸ I)) 1

Tactic:
LinearMap.ext (tensorQuotEquivQuotSMul_symm_mk I)

Premises used: LinearMap.ext, TensorProduct.tensorQuotEquivQuotSMul_symm_mk
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
⊢ (↑(tensorQuotEquivQuotSMul M I) : M ⊗[R] (R ⧸ I) →ₗ[R] M ⧸ I • ⊤) ∘ₗ
      (LinearMap.flip (mk R M (R ⧸ I)) : (a : R ⧸ I) → M →ₗ[R] M ⊗[R] (R ⧸ I)) 1 =
    (HSMul.hSMul (β := Submodule R M) I ⊤).mkQ

Tactic:
Eq.symm <| (LinearEquiv.toLinearMap_symm_comp_eq _ _).mp <|
    tensorQuotEquivQuotSMul_symm_comp_mkQ I

Premises used: LinearEquiv.toLinearMap_symm_comp_eq, Iff.mp, Eq.symm, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ
-- 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
S : Type u_4
inst_5 : CommRing S
inst_6 : Algebra R S
I : Ideal R
⊢ HSMul.hSMul (β := Submodule R S) I ⊤ = Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I)

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
S : Type u_4
inst_5 : CommRing S
inst_6 : Algebra R S
I : Ideal R
m : S
x : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
a : S
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (↑(LinearEquiv.symm
              (tensorQuotEquivQuotSMul S I ≪≫ₗ
                  (HSMul.hSMul (β := Submodule R S) I ⊤).quotEquivOfEq
                    (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (F := R →+* S) (algebraMap R S) I))) :
          S ⧸ Ideal.map (algebraMap R S) I →ₗ[R] S ⊗[R] (R ⧸ I)))
      (HSMul.hSMul (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) m
        (Quot.mk (⇑(Submodule.quotientRel (Ideal.map (algebraMap R S) I)) : S → S → Prop) a)) =
    HSMul.hSMul (α := S) (β := S ⊗[R] (R ⧸ I)) ((RingHom.id S : (a : S) → S) m : S)
      (AddHom.toFun (M := HasQuotient.Quotient S (B := Submodule S S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (LinearMap.toAddHom
            (↑(LinearEquiv.symm
                  (tensorQuotEquivQuotSMul S I ≪≫ₗ
                      (HSMul.hSMul (β := Submodule R S) I ⊤).quotEquivOfEq
                        (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) I)) ⋯ ≪≫ₗ
                    Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (F := R →+* S) (algebraMap R S) I))) :
              S ⧸ Ideal.map (algebraMap R S) I →ₗ[R] S ⊗[R] (R ⧸ I)))
          (Quot.mk (⇑(Submodule.quotientRel (Ideal.map (algebraMap R S) I)) : S → S → Prop) a) :
        S ⊗[R] (R ⧸ I))

Tactic:
congr
-- 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
m : A
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
        (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
          M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
      (HSMul.hSMul (β := TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n)) m 0) =
    HSMul.hSMul (α := A) (β :=
      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))))
      ((RingHom.id A : (a : A) → A) m : A)
      ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
          (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
            M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
        0)

Tactic:
simp
-- 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
m : A
x : M
y : N
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
        (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
          M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
      ((m • x) ⊗ₜ[R] Submodule.Quotient.mk y) =
    HSMul.hSMul (α := A) (β :=
      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))))
      ((RingHom.id A : (a : A) → A) m : A)
      ((TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n) :
            (a : M ⊗[R] (N ⧸ Submodule.restrictScalars R n)) →
              M ⊗[R] N ⧸ (TensorProduct.map LinearMap.id (Submodule.restrictScalars R n).subtype).range)
          (x ⊗ₜ[R] Submodule.Quotient.mk y) :
        HasQuotient.Quotient (M ⊗[R] N) (B := Submodule R (M ⊗[R] N))
          (LinearMap.range (M := TensorProduct.{u_1, u_4, u_5} R M ↥(Submodule.restrictScalars R n))
            (TensorProduct.map LinearMap.id (Submodule.subtype (Submodule.restrictScalars R n)))))

Tactic:
rfl
-- 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 (α := TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n))
    ((LinearEquiv.symm (tensorQuotientEquiv A B M n) :
          (a :
              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) →
            M ⊗[R] (N ⧸ n))
        (Submodule.Quotient.mk (x ⊗ₜ[R] y)) :
      TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n))
    (x ⊗ₜ[R] Submodule.Quotient.mk y : TensorProduct.{u_1, u_4, u_5} R M (N ⧸ n))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Submodule.restrictScalars, List.foldl, Submodule.quotientRel, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
⊢ Eq (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})

Tactic:
(Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm

Premises used: TensorProduct.mapOfCompatibleSMul, Submodule.span_eq_of_le, LinearMap.ker, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
refine_1 :
  {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x} ⊆
    (↑(LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N)) : Set (M ⊗[R] N))
refine_2 :
  LE.le (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})
⊢ Eq (α := Submodule A (M ⊗[R] N)) (LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N))
    (Submodule.span A
      {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x})

Tactic:
refine (Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm

Premises used: TensorProduct.mapOfCompatibleSMul, Submodule.span_eq_of_le, LinearMap.ker, Eq.symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
a : A
m : M
n : N
⊢ HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) ∈
    (↑(LinearMap.ker (M₂ := M ⊗[A] N) (mapOfCompatibleSMul A R A M N)) : Set (M ⊗[R] N))

Tactic:
simp [smul_tmul]

Premises used: TensorProduct.smul_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
m : M
x x_1 : N
⊢ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] (x + x_1)) =
    HAdd.hAdd (α := M ⊗[R] N ⧸ S) (β := M ⊗[R] N ⧸ S)
      ((S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] x) : M ⊗[R] N ⧸ S)
      ((S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] x_1) : M ⊗[R] N ⧸ S)

Tactic:
simp [tmul_add]

Premises used: TensorProduct.tmul_add
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
m : M
a : A
n : N
rw : HSMul.hSMul (β := M ⊗[R] N) a (m ⊗ₜ[R] n) - m ⊗ₜ[R] (a • n) ∈ S
⊢ (S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] (a • n)) =
    HSMul.hSMul (α := A) (β := M ⊗[R] N ⧸ S) ((RingHom.id A : (a : A) → A) a : A)
      ((S.mkQ : (a : M ⊗[R] N) → M ⊗[R] N ⧸ S) (m ⊗ₜ[R] n) : M ⊗[R] N ⧸ S)

Tactic:
rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
            Submodule.Quotient.eq, RingHom.id_apply]

Premises used: Submodule.Quotient.eq, RingHom.id_apply, Submodule.Quotient.mk_smul, Submodule.mkQ_apply, eq_comm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Quotient
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Type u_5
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module A N
inst_10 : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) :=
  Submodule.span A
    {x : M ⊗[R] N | ∃ (a : A) (m : M) (n : N), HSub.hSub (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n)) = x}
m : M
a : A
n : N
⊢ HSMul.hSMul (β := M ⊗[R] N) a (m ⊗ₜ[R] n) - m ⊗ₜ[R] (a • n) ∈ S

Tactic:
Submodule.subset_span ⟨a, m, n, rfl⟩

Premises used: Set.Mem, Exists.intro, Submodule.subset_span, rfl