awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
suffices : HSMul.hSMul (β := M ⊗[R] N) q.den ((q • m) ⊗ₜ[R] n) = HSMul.hSMul (β := M ⊗[R] N) q.den (m ⊗ₜ[R] (q • n))
⊢ Eq (α := M ⊗[R] N) ((q • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q • n))

Tactic:
suffices q.den • ((q • m) ⊗ₜ[R] n) = q.den • (m ⊗ₜ[R] (q • n)) from
      smul_right_injective (M ⊗[R] N) q.den_nz <| by norm_cast
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
rw : Eq (α := M ⊗[R] N) (HSMul.hSMul (α := ℚ) (↑q.num : ℚ) m ⊗ₜ[R] n) (m ⊗ₜ[R] HSMul.hSMul (α := ℚ) (↑q.num : ℚ) n)
⊢ HSMul.hSMul (β := M ⊗[R] N) q.den ((q • m) ⊗ₜ[R] n) = HSMul.hSMul (β := M ⊗[R] N) q.den (m ⊗ₜ[R] (q • n))

Tactic:
rw [smul_tmul', ← tmul_smul, ← smul_assoc, ← smul_assoc, nsmul_eq_mul, Rat.den_mul_eq_num]

Premises used: smul_assoc, TensorProduct.tmul_smul, TensorProduct.smul_tmul', nsmul_eq_mul, Rat.den_mul_eq_num
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
norm_cast : Eq (α := M ⊗[R] N) ((q.num • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q.num • n))
⊢ Eq (α := M ⊗[R] N) (HSMul.hSMul (α := ℚ) (↑q.num : ℚ) m ⊗ₜ[R] n) (m ⊗ₜ[R] HSMul.hSMul (α := ℚ) (↑q.num : ℚ) n)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R_1 : Type uR
R' : Type u_1
S_1 : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : Semiring A_1
inst_4 : Algebra R_1 A_1
inst_5 : Algebra S_1 A_1
inst_6 : IsScalarTower R_1 S_1 A_1
inst_7 : Semiring B_1
inst_8 : Algebra R_1 B_1
inst_9 : Semiring C
inst_10 : Algebra R_1 C
inst_11 : Algebra S_1 C
inst_12 : IsScalarTower R_1 S_1 C
inst_13 : Semiring D
inst_14 : Algebra R_1 D
inst_15 : Semiring E
inst_16 : Algebra R_1 E
inst_17 : Algebra S_1 E
inst_18 : IsScalarTower R_1 S_1 E
inst_19 : Semiring F
inst_20 : Algebra R_1 F
R_2 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R_2
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R_2 A
inst_27 : Algebra R_2 B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R_2 T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R_2 S A
inst_34 : CompatibleSMul R_2 S A B
inst_35 : Algebra R_2 S
inst_36 : CompatibleSMul R_2 S S A
inst_37 : CompatibleSMul S R_2 S A
R : Type u_8
M : Type u_9
N : Type u_10
inst_38 : CommSemiring R
inst_39 : AddCommGroup M
inst_40 : AddCommGroup N
inst_41 : Module R M
inst_42 : Module R N
inst_43 : Module ℚ M
inst_44 : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
rw rw₁ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] (q.num • n)) (m ⊗ₜ[R] (q.num • n))
⊢ Eq (α := M ⊗[R] N) ((q.num • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (q.num • n))

Tactic:
rw [smul_tmul]

Premises used: TensorProduct.smul_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := A ⊗[R] B ≃ₗ[R] B ⊗[R] A) (↑(TensorProduct.comm R A B) : A ⊗[R] B ≃ₗ[R] B ⊗[R] A)
    (_root_.TensorProduct.comm R A B)

Tactic:
rfl

Premises used: TensorProduct.comm, Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, AlgEquiv.toLinearEquiv, TensorProduct, TensorProduct.lift, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A
b : B
⊢ Eq (α := B ⊗[R] A) ((TensorProduct.comm R A B : (a : A ⊗[R] B) → B ⊗[R] A) (a ⊗ₜ[R] b) : B ⊗[R] A)
    (b ⊗ₜ[R] a : B ⊗[R] A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : A
b : B
⊢ Eq (α := A ⊗[R] B) ((AlgEquiv.symm (TensorProduct.comm R A B) : (a : B ⊗[R] A) → A ⊗[R] B) (b ⊗ₜ[R] a) : A ⊗[R] B)
    (a ⊗ₜ[R] b : A ⊗[R] B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
h :
  ∀ (a : B ⊗[R] A),
    Eq (α := A ⊗[R] B) ((AlgEquiv.symm (TensorProduct.comm R A B) : (a : B ⊗[R] A) → A ⊗[R] B) a : A ⊗[R] B)
      ((TensorProduct.comm R B A : (a : B ⊗[R] A) → A ⊗[R] B) a : A ⊗[R] B)
⊢ Eq (α := B ⊗[R] A ≃ₐ[R] A ⊗[R] B) (AlgEquiv.symm (TensorProduct.comm R A B)) (TensorProduct.comm R B A)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
a : B ⊗[R] A
⊢ Eq (α := A ⊗[R] B) ((AlgEquiv.symm (TensorProduct.comm R A B) : (a : B ⊗[R] A) → A ⊗[R] B) a : A ⊗[R] B)
    ((TensorProduct.comm R B A : (a : B ⊗[R] A) → A ⊗[R] B) a : A ⊗[R] B)

Tactic:
rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := A →ₐ[R] B ⊗[R] A) (AlgHom.comp (↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) includeLeft)
    includeRight

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AlgHom.comp, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := B →ₐ[R] B ⊗[R] A) (AlgHom.comp (↑(TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) includeRight)
    includeLeft

Tactic:
rfl

Premises used: Algebra.TensorProduct.includeLeftRingHom, Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.includeLeft, List.foldl, TensorProduct.tmul, AlgHom.comp, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
⊢ Eq (α := Subalgebra R (A ⊗[R] B)) (adjoin R {t : A ⊗[R] B | ∃ (a : A) (b : B), a ⊗ₜ[R] b = t}) ⊤

Tactic:
top_le_iff.mp <| (top_le_iff.mpr <| span_tmul_eq_top R A B).trans (span_le_adjoin R _)

Premises used: Iff.mpr, TensorProduct.span_tmul_eq_top, Algebra.span_le_adjoin, top_le_iff, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
s : S
a : A
⊢ Eq (α := A ⊗[R] S) ((commRight R S A : (a : S ⊗[R] A) → A ⊗[R] S) (s ⊗ₜ[R] a) : A ⊗[R] S) (a ⊗ₜ[R] s : A ⊗[R] S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
s : S
a : A
⊢ Eq (α := S ⊗[R] A) ((AlgEquiv.symm (commRight R S A) : (a : A ⊗[R] S) → S ⊗[R] A) (a ⊗ₜ[R] s) : S ⊗[R] A)
    (s ⊗ₜ[R] a : S ⊗[R] A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
inst_21 : CommSemiring T
inst_22 : Algebra R T
inst_23 : Algebra S T
inst_24 : Algebra T A
inst_25 : IsScalarTower R T A
inst_26 : IsScalarTower S T A
⊢ Eq (α := A ⊗[S] (C ⊗[R] D))
    (((AlgebraTensorModule.assoc R S T A C D : A ⊗[S] C ⊗[R] D ≃ₗ[T] A ⊗[S] (C ⊗[R] D)) :
        (a : A ⊗[S] C ⊗[R] D) → A ⊗[S] (C ⊗[R] D))
      1)
    1

Tactic:
simp [Algebra.TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
T : Type u_2
A : Type uA
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Algebra S C
inst_10 : IsScalarTower R S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : CommSemiring T
inst_14 : Algebra R T
inst_15 : Algebra S T
inst_16 : Algebra T A
inst_17 : IsScalarTower R T A
inst_18 : IsScalarTower S T A
⊢ Eq (α := A ⊗[S] C ⊗[R] D ≃ₗ[T] A ⊗[S] (C ⊗[R] D))
    ((↑(TensorProduct.assoc R S T A C D) : A ⊗[S] C ⊗[R] D ≃ₗ[T] A ⊗[S] (C ⊗[R] D)) :
      A ⊗[S] C ⊗[R] D ≃ₗ[T] A ⊗[S] (C ⊗[R] D))
    (AlgebraTensorModule.assoc R S T A C D : A ⊗[S] C ⊗[R] D ≃ₗ[T] A ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, AlgEquiv.toLinearEquiv, TensorProduct, rfl, TensorProduct.AlgebraTensorModule.assoc, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
T : Type u_2
A : Type uA
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Algebra S C
inst_10 : IsScalarTower R S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : CommSemiring T
inst_14 : Algebra R T
inst_15 : Algebra S T
inst_16 : Algebra T A
inst_17 : IsScalarTower R T A
inst_18 : IsScalarTower S T A
a : A
b : C
c : D
⊢ Eq (α := A ⊗[S] (C ⊗[R] D))
    (((TensorProduct.assoc R S T A C D : A ⊗[S] C ⊗[R] D ≃ₐ[T] A ⊗[S] (C ⊗[R] D)) :
          (a : A ⊗[S] C ⊗[R] D) → A ⊗[S] (C ⊗[R] D))
        (a ⊗ₜ[S] b ⊗ₜ[R] c) :
      A ⊗[S] (C ⊗[R] D))
    (a ⊗ₜ[S] (b ⊗ₜ[R] c) : A ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
T : Type u_2
A : Type uA
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Algebra S C
inst_10 : IsScalarTower R S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : CommSemiring T
inst_14 : Algebra R T
inst_15 : Algebra S T
inst_16 : Algebra T A
inst_17 : IsScalarTower R T A
inst_18 : IsScalarTower S T A
a : A
b : C
c : D
⊢ Eq (α := A ⊗[S] C ⊗[R] D)
    (((AlgEquiv.symm (TensorProduct.assoc R S T A C D) : A ⊗[S] (C ⊗[R] D) ≃ₐ[T] A ⊗[S] C ⊗[R] D) :
          (a : A ⊗[S] (C ⊗[R] D)) → A ⊗[S] C ⊗[R] D)
        (a ⊗ₜ[S] (b ⊗ₜ[R] c)) :
      A ⊗[S] C ⊗[R] D)
    (a ⊗ₜ[S] b ⊗ₜ[R] c : A ⊗[S] C ⊗[R] D)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A_1
inst_4 : Algebra R A_1
inst_5 : Algebra S A_1
inst_6 : IsScalarTower R S A_1
inst_7 : Semiring B_1
inst_8 : Algebra R B_1
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
T : Type u_3
A : Type u_4
B : Type u_5
inst_21 : CommSemiring T
inst_22 : CommSemiring A
inst_23 : CommSemiring B
inst_24 : Algebra R T
inst_25 : Algebra R A
inst_26 : Algebra R B
inst_27 : Algebra T A
inst_28 : IsScalarTower R T A
inst_29 : Algebra S A
inst_30 : IsScalarTower R S A
inst_31 : Algebra S T
inst_32 : IsScalarTower S T A
⊢ Eq (α := A ⊗[S] (S ⊗[R] B))
    (((LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R S T A B) : A ⊗[R] B ≃ₗ[T] A ⊗[S] (S ⊗[R] B)) :
        (a : A ⊗[R] B) → A ⊗[S] (S ⊗[R] B))
      1)
    1

Tactic:
simp [Algebra.TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T_1 : Type u_2
A_1 : Type uA
B_1 : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A_1
inst_4 : Algebra R A_1
inst_5 : Algebra S A_1
inst_6 : IsScalarTower R S A_1
inst_7 : Semiring B_1
inst_8 : Algebra R B_1
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
T : Type u_3
A : Type u_4
B : Type u_5
inst_21 : CommSemiring T
inst_22 : CommSemiring A
inst_23 : CommSemiring B
inst_24 : Algebra R T
inst_25 : Algebra R A
inst_26 : Algebra R B
inst_27 : Algebra T A
inst_28 : IsScalarTower R T A
inst_29 : Algebra S A
inst_30 : IsScalarTower R S A
inst_31 : Algebra S T
inst_32 : IsScalarTower S T A
x x_1 : A
x_2 x_3 : B
⊢ (((↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R S T A B)) : A ⊗[R] B →ₗ[T] A ⊗[S] (S ⊗[R] B)) :
          A ⊗[R] B →ₗ[T] A ⊗[S] (S ⊗[R] B)) :
        (a : A ⊗[R] B) → A ⊗[S] (S ⊗[R] B))
      ((x * x_1) ⊗ₜ[R] (x_2 * x_3)) =
    HMul.hMul (α := A ⊗[S] (S ⊗[R] B)) (β := A ⊗[S] (S ⊗[R] B))
      ((((↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R S T A B)) : A ⊗[R] B →ₗ[T] A ⊗[S] (S ⊗[R] B)) :
              A ⊗[R] B →ₗ[T] A ⊗[S] (S ⊗[R] B)) :
            (a : A ⊗[R] B) → A ⊗[S] (S ⊗[R] B))
          (x ⊗ₜ[R] x_2) :
        A ⊗[S] (S ⊗[R] B))
      ((((↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R S T A B)) : A ⊗[R] B →ₗ[T] A ⊗[S] (S ⊗[R] B)) :
              A ⊗[R] B →ₗ[T] A ⊗[S] (S ⊗[R] B)) :
            (a : A ⊗[R] B) → A ⊗[S] (S ⊗[R] B))
          (x_1 ⊗ₜ[R] x_3) :
        A ⊗[S] (S ⊗[R] B))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
A : Type u_4
B : Type u_5
inst_3 : CommSemiring T
inst_4 : CommSemiring A
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra T A
inst_10 : IsScalarTower R T A
inst_11 : Algebra S A
inst_12 : IsScalarTower R S A
inst_13 : Algebra S T
inst_14 : IsScalarTower S T A
a : A
s : S
b : B
⊢ Eq (α := A ⊗[R] B)
    (((cancelBaseChange R S T A B : A ⊗[S] (S ⊗[R] B) ≃ₐ[T] A ⊗[R] B) : (a : A ⊗[S] (S ⊗[R] B)) → A ⊗[R] B)
        (a ⊗ₜ[S] (s ⊗ₜ[R] b)) :
      A ⊗[R] B)
    ((s • a) ⊗ₜ[R] b : A ⊗[R] B)

Tactic:
TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul R S T a b s

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
A : Type u_4
B : Type u_5
inst_3 : CommSemiring T
inst_4 : CommSemiring A
inst_5 : CommSemiring B
inst_6 : Algebra R T
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Algebra T A
inst_10 : IsScalarTower R T A
inst_11 : Algebra S A
inst_12 : IsScalarTower R S A
inst_13 : Algebra S T
inst_14 : IsScalarTower S T A
a : A
b : B
⊢ Eq (α := A ⊗[S] (S ⊗[R] B))
    (((AlgEquiv.symm (cancelBaseChange R S T A B) : A ⊗[R] B ≃ₐ[T] A ⊗[S] (S ⊗[R] B)) :
          (a : A ⊗[R] B) → A ⊗[S] (S ⊗[R] B))
        (a ⊗ₜ[R] b) :
      A ⊗[S] (S ⊗[R] B))
    (a ⊗ₜ[S] (1 ⊗ₜ[R] b) : A ⊗[S] (S ⊗[R] B))

Tactic:
TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul R S T a b

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    ((AlgebraTensorModule.map f.toLinearMap g.toLinearMap : A ⊗[R] B →ₗ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D)
        ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C ⊗[R] D) (β := C ⊗[R] D)
        (((AlgebraTensorModule.map f.toLinearMap g.toLinearMap : A ⊗[R] B →ₗ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D)
            (a₁ ⊗ₜ[R] b₁) :
          C ⊗[R] D)
        (((AlgebraTensorModule.map f.toLinearMap g.toLinearMap : A ⊗[R] B →ₗ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D)
            (a₂ ⊗ₜ[R] b₂) :
          C ⊗[R] D)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
inst_15 : Semiring E
inst_16 : Algebra R E
inst_17 : Algebra S E
inst_18 : IsScalarTower R S E
inst_19 : Semiring F
inst_20 : Algebra R F
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ Eq (α := C ⊗[R] D)
    (((AlgebraTensorModule.map f.toLinearMap g.toLinearMap : A ⊗[R] B →ₗ[S] C ⊗[R] D) : (a : A ⊗[R] B) → C ⊗[R] D)
        (1 ⊗ₜ[R] 1) :
      C ⊗[R] D)
    (1 : C ⊗[R] D)

Tactic:
simp [one_def]

Premises used: Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
inst_13 : Semiring D
inst_14 : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ Eq (α := A ⊗[R] B →ₗ[S] C ⊗[R] D) (AlgHom.toLinearMap (map f g) : A ⊗[R] B →ₗ[S] C ⊗[R] D)
    (AlgebraTensorModule.map f.toLinearMap g.toLinearMap : A ⊗[R] B →ₗ[S] C ⊗[R] D)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, Quotient.liftOn', AddCon.liftOn, TensorProduct, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift