awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne A
inst_2 : Module R A
inst_3 : AddCommMonoidWithOne B
inst_4 : Module R B
n : ℕ
rw : Eq (α := A ⊗[R] B) ((↑n : A) ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
rw₁ : Eq (α := A ⊗[R] B) (HSMul.hSMul (β := A) n 1 ⊗ₜ[R] 1) (1 ⊗ₜ[R] (↑n : B))
rw₂ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] HSMul.hSMul (β := B) n 1) (1 ⊗ₜ[R] (↑n : B))
rw₃ rw₄ : Eq (α := A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B)) (1 ⊗ₜ[R] (↑n : B))
⊢ Eq (α := A ⊗[R] B) (↑n : A ⊗[R] B) (1 ⊗ₜ[R] (↑n : B))

Tactic:
rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.natCast_def, nsmul_one
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a₁ a₂ : A
b₁ b₂ : B
⊢ Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        (a₂ ⊗ₜ[R] b₂) :
      A ⊗[R] B)
    ((a₁ * a₂) ⊗ₜ[R] (b₁ * 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.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a₁ a₂ : A
b₁ b₂ : B
⊢ HMul.hMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a₁ a₂ a₃ : A
b₁ b₂ b₃ : B
ha : SemiconjBy a₁ a₂ a₃
hb : SemiconjBy b₁ b₂ b₃
⊢ SemiconjBy (M := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃)

Tactic:
congr_arg₂ (· ⊗ₜ[R] ·) ha.eq hb.eq

Premises used: Quotient.liftOn', AddCon.liftOn, SemiconjBy, SemiconjBy.eq, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, congr_arg₂
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a₁ a₂ : A
b₁ b₂ : B
ha : Commute a₁ a₂
hb : Commute b₁ b₂
⊢ Commute (S := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)

Tactic:
ha.tmul hb

Premises used: SemiconjBy.tmul, Commute
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a b c : A ⊗[R] B
⊢ a * (b + c) = a * b + a * c

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a b c : A ⊗[R] B
⊢ (a + b) * c = a * c + b * c

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a : A ⊗[R] B
⊢ 0 * a = 0

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
a : A ⊗[R] B
⊢ a * 0 = 0

Tactic:
simp [HMul.hMul, Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • x * 0 = r • (x * 0)

Tactic:
simp [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
⊢ HSMul.hSMul (β := A ⊗[R] B) r 0 * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b)

Tactic:
simp [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul : HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul :
  HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))
tmul₁ : HMul.hMul (α := A ⊗[R] B) ((r • a') ⊗ₜ[R] b') (a ⊗ₜ[R] b) = (r • (a' * a)) ⊗ₜ[R] (b' * b)
tmul₂ : Eq (α := A ⊗[R] B) ((r • a' * a) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
tmul₃ tmul₄ : Eq (α := A ⊗[R] B) ((r • (a' * a)) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
⊢ HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b))

Tactic:
rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]

Premises used: smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
x y : A ⊗[R] B
hx : r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
hy : r • y * a ⊗ₜ[R] b = r • (y * a ⊗ₜ[R] b)
⊢ r • (x + y) * a ⊗ₜ[R] b = r • ((x + y) * a ⊗ₜ[R] b)

Tactic:
simp [smul_add, add_mul _, *]

Premises used: add_mul, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
tmul : HSMul.hSMul (β := A ⊗[R] B) r 0 * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b)
tmul₁ :
  ∀ (a' : A) (b' : B),
    HSMul.hSMul (β := A ⊗[R] B) r (a' ⊗ₜ[R] b') * a ⊗ₜ[R] b = r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b)
tmul₂ :
  ∀ (x y : A ⊗[R] B) (hx : r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)) (hy : r • y * a ⊗ₜ[R] b = r • (y * a ⊗ₜ[R] b)),
    r • (x + y) * a ⊗ₜ[R] b = r • ((x + y) * a ⊗ₜ[R] b)
⊢ r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)

Tactic:
induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
      | add x y hx hy => simp [smul_add, add_mul _, *]

Premises used: add_mul, smul_zero, smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.smul_tmul', TensorProduct.tmul, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
x_1 x y : A ⊗[R] B
hx : r • x_1 * x = r • (x_1 * x)
hy : r • x_1 * y = r • (x_1 * y)
⊢ r • x_1 * (x + y) = r • (x_1 * (x + y))

Tactic:
simp [smul_add, mul_add _, *]

Premises used: mul_add, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : IsScalarTower S A A
inst_12 : SMulCommClass R S A
r : S
x y : A ⊗[R] B
zero : r • x * 0 = r • (x * 0)
tmul : ∀ (a : A) (b : B), r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
add :
  ∀ (x_1 y : A ⊗[R] B) (hx : r • x * x_1 = r • (x * x_1)) (hy : r • x * y = r • (x * y)),
    r • x * (x_1 + y) = r • (x * (x_1 + y))
⊢ r • x * y = r • (x * y)

Tactic:
induction y with
    | zero => simp [smul_zero]
    | tmul a b => induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
      | add x y hx hy => simp [smul_add, add_mul _, *]
    | add x y hx hy => simp [smul_add, mul_add _, *]

Premises used: add_mul, smul_zero, smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.smul_tmul', mul_add, TensorProduct.tmul, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • (x * 0) = x * HSMul.hSMul (β := A ⊗[R] B) r 0

Tactic:
simp [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
⊢ r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b) = 0 * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)

Tactic:
simp [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul : HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
⊢ r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
tmul : (r • (a' * a)) ⊗ₜ[R] (b' * b) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
tmul₁ : (r • (a' * a)) ⊗ₜ[R] (b' * b) = HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') ((r • a) ⊗ₜ[R] b)
tmul₂ : Eq (α := A ⊗[R] B) ((r • (a' * a)) ⊗ₜ[R] (b' * b)) ((a' * r • a) ⊗ₜ[R] (b' * b))
tmul₃ tmul₄ : Eq (α := A ⊗[R] B) ((r • (a' * a)) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
⊢ HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)

Tactic:
rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.smul_tmul', mul_smul_comm
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
a : A
b : B
x y : A ⊗[R] B
hx : r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
hy : r • (y * a ⊗ₜ[R] b) = y * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
⊢ r • ((x + y) * a ⊗ₜ[R] b) = (x + y) * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)

Tactic:
simp [smul_add, add_mul _, *]

Premises used: add_mul, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
tmul : r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b) = 0 * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
tmul₁ :
  ∀ (a' : A) (b' : B),
    r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
tmul₂ :
  ∀ (x y : A ⊗[R] B) (hx : r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b))
    (hy : r • (y * a ⊗ₜ[R] b) = y * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)),
    r • ((x + y) * a ⊗ₜ[R] b) = (x + y) * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
⊢ r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)

Tactic:
induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
      | add x y hx hy => simp [smul_add, add_mul _, *]

Premises used: add_mul, smul_zero, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.smul_tmul', mul_smul_comm, TensorProduct.tmul, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
x_1 x y : A ⊗[R] B
hx : r • (x_1 * x) = x_1 * r • x
hy : r • (x_1 * y) = x_1 * r • y
⊢ r • (x_1 * (x + y)) = x_1 * r • (x + y)

Tactic:
simp [smul_add, mul_add _, *]

Premises used: mul_add, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
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 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
inst_9 : Monoid S
inst_10 : DistribMulAction S A
inst_11 : SMulCommClass S A A
inst_12 : SMulCommClass R S A
r : S
x y : A ⊗[R] B
zero : r • (x * 0) = x * HSMul.hSMul (β := A ⊗[R] B) r 0
tmul : ∀ (a : A) (b : B), r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
add :
  ∀ (x_1 y : A ⊗[R] B) (hx : r • (x * x_1) = x * r • x_1) (hy : r • (x * y) = x * r • y),
    r • (x * (x_1 + y)) = x * r • (x_1 + y)
⊢ r • (x * y) = x * r • y

Tactic:
induction y with
    | zero => simp [smul_zero]
    | tmul a b => induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
      | add x y hx hy => simp [smul_add, add_mul _, *]
    | add x y hx hy => simp [smul_add, mul_add _, *]

Premises used: add_mul, smul_zero, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.smul_tmul', mul_smul_comm, mul_add, TensorProduct.tmul, smul_add
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      x =
    x

Tactic:
TensorProduct.induction_on x ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
refine_1 :
  Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
        (a : A ⊗[R] B) → A ⊗[R] B)
      0)
    0
refine_2 :
  ∀ (x : A) (y : B),
    Eq (α := A ⊗[R] B)
      ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          (x ⊗ₜ[R] y) :
        A ⊗[R] B)
      (x ⊗ₜ[R] y : A ⊗[R] B)
refine_3 :
  ∀ (x y : A ⊗[R] B),
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          x =
        x →
      (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B) → A ⊗[R] B)
            y =
          y →
        (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
              (a : A ⊗[R] B) → A ⊗[R] B)
            (x + y) =
          x + y
⊢ (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      x =
    x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
        (a : A ⊗[R] B) → A ⊗[R] B)
      0)
    0

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : NonAssocSemiring B
inst_6 : Module R B
inst_7 : SMulCommClass R B B
inst_8 : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B),
    Eq (α := A ⊗[R] B)
      ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          (x ⊗ₜ[R] y) :
        A ⊗[R] B)
      (x ⊗ₜ[R] y : A ⊗[R] B)

Tactic:
simp +contextual