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_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₃
x : M₁
z : M₂
⊢ HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z : M₁₂) =
    (((f : (a : M₁) → M₂ →ₗ[S] M₁₂) (t • x) : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z

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 : M₃
x : M₁
z : M₂
⊢ HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z : M₁₂) =
    (((f : (a : M₁) → M₂ →ₗ[S] M₁₂) (t • x) : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z

Tactic:
have : t • (f x) z = f (t • x) z := by 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 : M₃
x : M₁
z : M₂
this :
  HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[S] M₁₂) x : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z : M₁₂) =
    (((f : (a : M₁) → M₂ →ₗ[S] M₁₂) (t • x) : M₂ →ₗ[S] M₁₂) : (a : M₂) → M₁₂) z
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:
dsimp
-- 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₃
x : M₁ ⊗[R] M₂
tmul : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
tmul₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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:
induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', TensorProduct.add_tmul, _private.0.IsTensorProduct.assocAux_tmul, TensorProduct.tmul, LinearMap.restrictScalars₁₂_apply_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_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₁₂ ⊗[S] M₃
zero : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
add : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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:
induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y =>
    obtain ⟨x, rfl⟩ := hf.equiv.surjective x
    induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', TensorProduct.add_tmul, _private.0.IsTensorProduct.assocAux_tmul, TensorProduct.tmul, LinearMap.restrictScalars₁₂_apply_apply, rfl
-- 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₂₃
T : Type u_16
inst_21 : CommSemiring T
inst_22 : Algebra R T
inst_23 : Module T M₁
inst_24 : IsScalarTower R T M₁
inst_25 : Module T M₁₂
inst_26 : SMulCommClass S T M₁₂
inst_27 : 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
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁ ⊗[R] M₂₃)
    ((assoc 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:
assocAux_tmul (f.restrictScalars₁₂ R S) hf g hg _ _ _

Premises used: LinearMap.restrictScalars₁₂, _private.0.IsTensorProduct.assocAux_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₂₃
T : Type u_16
inst_21 : CommSemiring T
inst_22 : Algebra R T
inst_23 : Module T M₁
inst_24 : IsScalarTower R T M₁
inst_25 : Module T M₁₂
inst_26 : SMulCommClass S T M₁₂
inst_27 : 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
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ Eq (α := M₁₂ ⊗[S] M₃)
    ((LinearEquiv.symm (assoc 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:
assocAux_symm_tmul (f.restrictScalars₁₂ R S) hf g hg _ _ _

Premises used: Quotient.liftOn', AddCon.liftOn, _private.0.IsTensorProduct.assocAux_symm_tmul, LinearMap.restrictScalars₁₂
-- 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_3 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf_2 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_3)
g_3 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_2 : IsTensorProduct g_3
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ :
  ∀ (t : T) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) (t • x) : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y =
      HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
h₂ :
  ∀ (s : S) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) (s • y) =
      HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
⊢ ∀ (m₁ m₂ : M₁) (n : M₂),
    (fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) (m₁ + m₂)
        n =
      HAdd.hAdd (α := M₁₂)
        ((fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m₁ n)
        ((fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m₂ n)

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_3 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf_2 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_3)
g_3 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_2 : IsTensorProduct g_3
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ :
  ∀ (t : T) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) (t • x) : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y =
      HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
h₂ :
  ∀ (s : S) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) (s • y) =
      HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
⊢ ∀ (c : T) (m : M₁) (n : M₂),
    (fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) (c • m) n =
      HSMul.hSMul (β := M₁₂) c
        ((fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m n)

Tactic:
simp [h₁]
-- 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_3 : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf_2 : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f_3)
g_3 : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg_2 : IsTensorProduct g_3
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ :
  ∀ (t : T) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) (t • x) : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y =
      HSMul.hSMul (β := M₁₂) t ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
h₂ :
  ∀ (s : S) (x : M₁) (y : M₂),
    (((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) (s • y) =
      HSMul.hSMul (β := M₁₂) s ((((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) y : M₁₂)
⊢ ∀ (m : M₁) (n₁ n₂ : M₂),
    (fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m
        (n₁ + n₂) =
      HAdd.hAdd (α := M₁₂)
        ((fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m n₁)
        ((fun (x : M₁) ↦ ((⇑((f : (a : M₁) → M₂ →ₗ[R] M₁₂) x : M₂ →ₗ[R] M₁₂) : (a : M₂) → M₁₂) : (a : M₂) → M₁₂)) m n₂)

Tactic:
simp