awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
have 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)
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 _, *]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ r • x * y = r • (x * y)
have zero : r • x * 0 = r • (x * 0)
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 _, *]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ r • x * y = r • (x * y)
have tmul : ∀ (a : A) (b : B), r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)
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 _, *]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ r • x * y = r • (x * y)
have 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))
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 _, *]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ r • HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') (a ⊗ₜ[R] b) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have tmul : HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have tmul : (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]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have tmul₁ : (r • (a' * a)) ⊗ₜ[R] (b' * b) = HMul.hMul (α := A ⊗[R] B) (a' ⊗ₜ[R] b') ((r • a) ⊗ₜ[R] b)
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have tmul₂ : Eq (α := A ⊗[R] B) ((r • (a' * a)) ⊗ₜ[R] (b' * b)) ((a' * r • a) ⊗ₜ[R] (b' * b))
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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))
⊢ HSMul.hSMul (β := A ⊗[R] B) r ((a' * a) ⊗ₜ[R] (b' * b)) = a' ⊗ₜ[R] b' * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have tmul₃ : Eq (α := A ⊗[R] B) ((r • (a' * a)) ⊗ₜ[R] (b' * b)) ((r • (a' * a)) ⊗ₜ[R] (b' * b))
Tactic: rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have tmul : r • HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b) = 0 * 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 _, *]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have 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)
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 _, *]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
have 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)
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 _, *]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ r • (x * y) = x * r • y
have zero : r • (x * 0) = x * HSMul.hSMul (β := A ⊗[R] B) r 0
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 _, *]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ r • (x * y) = x * r • y
have tmul : ∀ (a : A) (b : B), r • (x * a ⊗ₜ[R] b) = x * HSMul.hSMul (β := A ⊗[R] B) r (a ⊗ₜ[R] b)
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 _, *]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ r • (x * y) = x * r • y
have 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)
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 _, *]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
have 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
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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
⊢ (((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
have 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)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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)
⊢ (((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
have 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
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      (1 ⊗ₜ[R] 1) =
    x
have refine_1 : Eq (α := A ⊗[R] B)
  (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) 0 : (a : A ⊗[R] B) → A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B)
  (0 : A ⊗[R] B)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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) 0 : (a : A ⊗[R] B) → A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B)
    (0 : A ⊗[R] B)
⊢ (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      (1 ⊗ₜ[R] 1) =
    x
have refine_2 : ∀ (x : A) (y : B),
  Eq (α := A ⊗[R] B)
    ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x ⊗ₜ[R] y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
          (a : A ⊗[R] B) → A ⊗[R] B)
        (1 ⊗ₜ[R] 1) :
      A ⊗[R] B)
    (x ⊗ₜ[R] y : A ⊗[R] B)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
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) 0 : (a : A ⊗[R] B) → A ⊗[R] B) (1 ⊗ₜ[R] 1) : A ⊗[R] B)
    (0 : A ⊗[R] B)
refine_2 :
  ∀ (x : A) (y : B),
    Eq (α := A ⊗[R] B)
      ((((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x ⊗ₜ[R] y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) :
            (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) :
        A ⊗[R] B)
      (x ⊗ₜ[R] y : A ⊗[R] B)
⊢ (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
      (1 ⊗ₜ[R] 1) =
    x
have refine_3 : ∀ (x y : A ⊗[R] B),
  (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) x : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
        (1 ⊗ₜ[R] 1) =
      x →
    (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) y : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) =
        y →
      (((mul : (a : A ⊗[R] B) → A ⊗[R] B →ₗ[R] A ⊗[R] B) (x + y) : A ⊗[R] B →ₗ[R] A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B)
          (1 ⊗ₜ[R] 1) =
        x + y
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_