awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
rw :
  Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) (s • x)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        (HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x : M₁₂)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)

Tactic:
rw [← map_smul]

Premises used: map_smul
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) y : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) (s • x)) :
      M₁ ⊗[R] M₂)
    (y ⊗ₜ[R] (s • x) : M₁ ⊗[R] M₂)

Tactic:
apply hf.equiv_symm_apply

Premises used: IsTensorProduct.equiv_symm_apply
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this_1 : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
⊢ AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
      (HSMul.hSMul (β := M₂ ⊗[R] M₁) s 0) =
    HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) 0)

Tactic:
simp_all [TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this_1 : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂
y : M₁
⊢ AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
      (HSMul.hSMul (β := M₂ ⊗[R] M₁) s (x ⊗ₜ[R] y)) =
    HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (x ⊗ₜ[R] y))

Tactic:
simp_all [TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this_1 : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x y : M₂ ⊗[R] M₁
h :
  AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) x)
h_1 :
  AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • y) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) y)
⊢ AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • (x + y)) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (x + y))

Tactic:
simp_all [TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_9
S : Type u_10
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₁₂
inst_7 : AddCommMonoid M₂₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module S M₂
inst_11 : IsScalarTower R S M₂
inst_12 : Module R M₃
inst_13 : Module S M₃
inst_14 : IsScalarTower R S M₃
inst_15 : Module R M₁₂
inst_16 : Module S M₁₂
inst_17 : IsScalarTower R S M₁₂
inst_18 : Module R M₂₃
inst_19 : Module S M₂₃
inst_20 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁₂ ⊗[S] M₃)
    ((LinearEquiv.symm (assocAux f hf g hg) : (a : M₁ ⊗[R] M₂₃) → M₁₂ ⊗[S] M₃)
        (x₁ ⊗ₜ[R] (((g : (a : M₂) → M₃ →ₗ[S] M₂₃) x₂ : M₃ →ₗ[S] M₂₃) : (a : M₃) → M₂₃) x₃) :
      M₁₂ ⊗[S] M₃)
    ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x₁ : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x₂ ⊗ₜ[S] x₃ : M₁₂ ⊗[S] M₃)

Tactic:
simp [IsTensorProduct.assocAux]

Premises used: _private.0.IsTensorProduct.assocAux
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_9
S : Type u_10
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₁₂
inst_7 : AddCommMonoid M₂₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module S M₂
inst_11 : IsScalarTower R S M₂
inst_12 : Module R M₃
inst_13 : Module S M₃
inst_14 : IsScalarTower R S M₃
inst_15 : Module R M₁₂
inst_16 : Module S M₁₂
inst_17 : IsScalarTower R S M₁₂
inst_18 : Module R M₂₃
inst_19 : Module S M₂₃
inst_20 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x₁ : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x₂) :
      M₁ ⊗[R] M₂)
    (x₁ ⊗ₜ[R] x₂ : M₁ ⊗[R] M₂)

Tactic:
have : hf.equiv.symm (f x₁ x₂) = x₁ ⊗ₜ x₂ := hf.equiv_symm_apply _ _
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_9
S : Type u_10
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid M₁₂
inst_7 : AddCommMonoid M₂₃
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module S M₂
inst_11 : IsScalarTower R S M₂
inst_12 : Module R M₃
inst_13 : Module S M₃
inst_14 : IsScalarTower R S M₃
inst_15 : Module R M₁₂
inst_16 : Module S M₁₂
inst_17 : IsScalarTower R S M₁₂
inst_18 : Module R M₂₃
inst_19 : Module S M₂₃
inst_20 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
this :
  Eq (α := M₁ ⊗[R] M₂)
    ((hf.equiv.symm : (a : M₁₂) → M₁ ⊗[R] M₂)
        ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x₁ : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x₂) :
      M₁ ⊗[R] M₂)
    (x₁ ⊗ₜ[R] x₂ : M₁ ⊗[R] M₂)
⊢ Eq (α := M₁ ⊗[R] M₂₃)
    ((assocAux f hf g hg : (a : M₁₂ ⊗[S] M₃) → M₁ ⊗[R] M₂₃)
        ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x₁ : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) x₂ ⊗ₜ[S] x₃) :
      M₁ ⊗[R] M₂₃)
    (x₁ ⊗ₜ[R] (((g : (a : M₂) → M₃ →ₗ[S] M₂₃) x₂ : M₃ →ₗ[S] M₂₃) : (a : M₃) → M₂₃) x₃ : M₁ ⊗[R] M₂₃)

Tactic:
simp [IsTensorProduct.assocAux, this]

Premises used: _private.0.IsTensorProduct.assocAux
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x y : M₁₂ ⊗[S] M₃
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂
y : M₃
tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨x, rfl⟩ := hf.equiv.surjective x

Premises used: LinearEquiv.surjective, IsTensorProduct.equiv, rfl
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f_2 : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf_1 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_2)
g_2 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_1 : IsTensorProduct g_2
T : Type u_16
inst_36 : CommSemiring T
inst_37 : Algebra R T
inst_38 : Module T M₁
inst_39 : IsScalarTower R T M₁
inst_40 : Module T M₁₂
inst_41 : SMulCommClass S T M₁₂
inst_42 : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y_1 : M₃
x y : M₁ ⊗[R] M₂
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_all [add_tmul]

Premises used: TensorProduct.add_tmul