awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
a : A
⊢ (TensorProduct.lid R A : (a : R ⊗[R] A) → A) (r ⊗ₜ[R] a) = r • a

Tactic:
rfl

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

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, 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
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
⊢ Eq (α := A ⊗[R] R ≃ₗ[S] A) ((↑(TensorProduct.rid R S A) : A ⊗[R] R ≃ₗ[S] A) : A ⊗[R] R ≃ₗ[S] A)
    (AlgebraTensorModule.rid R S A : A ⊗[R] R ≃ₗ[S] A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.AlgebraTensorModule.rid, AlgEquiv.toLinearEquiv, TensorProduct, rfl, TensorProduct.AlgebraTensorModule.lift
-- 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
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
r : R
a : A
⊢ ((TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) (a ⊗ₜ[R] r) = r • a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, 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
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
a : A
⊢ Eq (α := A ⊗[R] R) (((AlgEquiv.symm (TensorProduct.rid R S A) : A ≃ₐ[S] A ⊗[R] R) : (a : A) → A ⊗[R] R) a : A ⊗[R] R)
    (a ⊗ₜ[R] 1 : A ⊗[R] R)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring B
inst_4 : Algebra R B
a :
  ∀ (x : S),
    Eq (α := S ⊗[R] B)
      (((((AlgebraTensorModule.curry
                    ((↑R :
                          {S M : Type uS} →
                            {M₂ : Type (max uB uS)} →
                              [inst : Semiring R] →
                                [inst_5 : Semiring S] →
                                  [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 : Module S M₂] →
                                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ
                      AlgEquiv.toLinearMap (TensorProduct.rid R R S)) :
                  S →ₗ[R] R →ₗ[R] S ⊗[R] B) :
                (a : S) → R →ₗ[R] S ⊗[R] B)
              x :
            R →ₗ[R] S ⊗[R] B) :
          (a : R) → S ⊗[R] B)
        1)
      (((((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R B)) : S →ₗ[R] R →ₗ[R] S ⊗[R] B) :
                (a : S) → R →ₗ[R] S ⊗[R] B)
              x :
            R →ₗ[R] S ⊗[R] B) :
          (a : R) → S ⊗[R] B)
        1)
⊢ Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] B)
    ((↑R :
            {S M : Type uS} →
              {M₂ : Type (max uB uS)} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [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 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ
        AlgEquiv.toLinearMap (TensorProduct.rid R R S) :
      S ⊗[R] R →ₗ[R] S ⊗[R] B)
    (LinearMap.lTensor S (Algebra.linearMap R B) : S ⊗[R] R →ₗ[R] S ⊗[R] B)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type uR
S : Type uS
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring B
inst_4 : Algebra R B
x : S
⊢ Eq (α := S ⊗[R] B)
    (((((AlgebraTensorModule.curry
                  ((↑R :
                        {S M : Type uS} →
                          {M₂ : Type (max uB uS)} →
                            [inst : Semiring R] →
                              [inst_5 : Semiring S] →
                                [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 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ
                    AlgEquiv.toLinearMap (TensorProduct.rid R R S)) :
                S →ₗ[R] R →ₗ[R] S ⊗[R] B) :
              (a : S) → R →ₗ[R] S ⊗[R] B)
            x :
          R →ₗ[R] S ⊗[R] B) :
        (a : R) → S ⊗[R] B)
      1)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R B)) : S →ₗ[R] R →ₗ[R] S ⊗[R] B) :
              (a : S) → R →ₗ[R] S ⊗[R] B)
            x :
          R →ₗ[R] S ⊗[R] B) :
        (a : R) → S ⊗[R] B)
      1)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
x : A
y : C
trans : x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = HSMul.hSMul (β := A ⊗[R] B ⊗[A] (A ⊗[R] C)) x (1 ⊗ₜ[A] (1 ⊗ₜ[R] y))
trans₁ : HSMul.hSMul (β := A ⊗[R] B ⊗[A] (A ⊗[R] C)) x (1 ⊗ₜ[A] (1 ⊗ₜ[R] y)) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)
⊢ Eq (α := A ⊗[R] B ⊗[A] (A ⊗[R] C)) (x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)) (1 ⊗ₜ[A] (x ⊗ₜ[R] y))

Tactic:
trans x • 1 ⊗ₜ[A] (1 ⊗ₜ[R] y)

Premises used: TensorProduct.tmul, OfNat.ofNat
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
x : A
y : C
⊢ HSMul.hSMul (β := A ⊗[R] B ⊗[A] (A ⊗[R] C)) x (1 ⊗ₜ[A] (1 ⊗ₜ[R] y)) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)

Tactic:
simp [← tmul_smul, smul_tmul' (M := A)]

Premises used: TensorProduct.tmul_smul, TensorProduct.smul_tmul'
-- 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 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R A
inst_27 : Algebra R B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R S A
inst_34 : CompatibleSMul R S A B
x : A ⊗[S] B
⊢ ∀ (y : A ⊗[S] B),
    ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
        (0 * y) =
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            0 :
          A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            y :
          A ⊗[R] B)

Tactic:
simp
-- 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 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R A
inst_27 : Algebra R B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R S A
inst_34 : CompatibleSMul R S A B
x : A ⊗[S] B
x_1 : A
x_2 : B
y : A ⊗[S] B
⊢ ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
      (HMul.hMul (α := A ⊗[S] B) (x_1 ⊗ₜ[S] x_2) 0) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          (x_1 ⊗ₜ[S] x_2) :
        A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B) 0 :
        A ⊗[R] B)

Tactic:
simp
-- 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 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R A
inst_27 : Algebra R B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R S A
inst_34 : CompatibleSMul R S A B
x : A ⊗[S] B
x_1 : A
x_2 : B
y : A ⊗[S] B
⊢ ∀ (x : A) (y : B),
    ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
        (HMul.hMul (α := A ⊗[S] B) (x_1 ⊗ₜ[S] x_2) (x ⊗ₜ[S] y)) =
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            (x_1 ⊗ₜ[S] x_2) :
          A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            (x ⊗ₜ[S] y) :
          A ⊗[R] B)

Tactic:
simp
-- 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 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R A
inst_27 : Algebra R B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R S A
inst_34 : CompatibleSMul R S A B
x : A ⊗[S] B
x_1 : A
x_2 : B
y x_3 x_4 : A ⊗[S] B
h :
  ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
      (x_1 ⊗ₜ[S] x_2 * x_3) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          (x_1 ⊗ₜ[S] x_2) :
        A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          x_3 :
        A ⊗[R] B)
h' :
  ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
      (x_1 ⊗ₜ[S] x_2 * x_4) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          (x_1 ⊗ₜ[S] x_2) :
        A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          x_4 :
        A ⊗[R] B)
⊢ ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
      (x_1 ⊗ₜ[S] x_2 * (x_3 + x_4)) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          (x_1 ⊗ₜ[S] x_2) :
        A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          (x_3 + x_4) :
        A ⊗[R] B)

Tactic:
simp only [mul_add, map_add, h, h']

Premises used: map_add, mul_add
-- 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 : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst_21 : CommSemiring R
inst_22 : CommSemiring S
inst_23 : CommSemiring T
inst_24 : Semiring A
inst_25 : Semiring B
inst_26 : Algebra R A
inst_27 : Algebra R B
inst_28 : Algebra S A
inst_29 : Algebra S B
inst_30 : Algebra T A
inst_31 : SMulCommClass R T A
inst_32 : SMulCommClass S T A
inst_33 : SMulCommClass R S A
inst_34 : CompatibleSMul R S A B
x x_1 x_2 : A ⊗[S] B
h :
  ∀ (y : A ⊗[S] B),
    ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
        (x_1 * y) =
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            x_1 :
          A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            y :
          A ⊗[R] B)
h' :
  ∀ (y : A ⊗[S] B),
    ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
        (x_2 * y) =
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            x_2 :
          A ⊗[R] B)
        (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
            y :
          A ⊗[R] B)
x_3 : A ⊗[S] B
⊢ ((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
      ((x_1 + x_2) * x_3) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          (x_1 + x_2) :
        A ⊗[R] B)
      (((_root_.TensorProduct.mapOfCompatibleSMul R S T A B : A ⊗[S] B →ₗ[T] A ⊗[R] B) : (a : A ⊗[S] B) → A ⊗[R] B)
          x_3 :
        A ⊗[R] B)

Tactic:
simp only [add_mul, map_add, h, h']

Premises used: add_mul, map_add
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : Algebra S B
inst_9 : Algebra T A
inst_10 : SMulCommClass R T A
inst_11 : SMulCommClass S T A
inst_12 : SMulCommClass R S A
inst_13 : CompatibleSMul R S A B
m : A
n : B
⊢ Eq (α := A ⊗[R] B) ((mapOfCompatibleSMul R S T A B : (a : A ⊗[S] B) → A ⊗[R] B) (m ⊗ₜ[S] n) : A ⊗[R] B)
    (m ⊗ₜ[R] n : 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 u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : Algebra S B
inst_9 : Algebra T A
inst_10 : SMulCommClass R T A
inst_11 : SMulCommClass S T A
inst_12 : SMulCommClass R S A
inst_13 : CompatibleSMul R S A B
⊢ Function.Surjective (α := A ⊗[S] B) (β := A ⊗[R] B) (⇑(mapOfCompatibleSMul R S T A B) : (a : A ⊗[S] B) → A ⊗[R] B)

Tactic:
_root_.TensorProduct.mapOfCompatibleSMul_surjective R S T A B

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.mapOfCompatibleSMul_surjective, TensorProduct
-- Module: Mathlib.RingTheory.TensorProduct.Maps
Goal:
R : Type u_3
S : Type u_4
A : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra S A
inst_5 : Algebra R S
inst_6 : CompatibleSMul R S S A
inst_7 : CompatibleSMul S R S A
s : S
a : A
⊢ (lidOfCompatibleSMul R S A : (a : S ⊗[R] A) → A) (s ⊗ₜ[R] a) = s • a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- 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
⊢ IsAddTorsionFree (M ⊗[R] N)

Tactic:
have : IsAddTorsionFree (M ⊗[R] N) := .of_module_rat _
-- 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_1 : IsAddTorsionFree (M ⊗[R] N)
this : 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) ((fun (x : M ⊗[R] N) ↦ q.den • x) ((q • m) ⊗ₜ[R] n))
    ((fun (x : M ⊗[R] N) ↦ q.den • x) (m ⊗ₜ[R] (q • n)))

Tactic:
norm_cast