awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
n : R
r : A
h :
  ∀ (x : B) (x_1 : M),
    Eq (α := M)
      ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (n • r)
                    (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                  (a : B) → Module.End R M)
                x :
              Module.End R M) :
            (a : M) → M)
          x_1 :
        M)
      ((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) n : R)
                    (HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
                      (AlgHom.toLinearMap (Algebra.lsmul R R M))) :
                  (a : B) → Module.End R M)
                x :
              Module.End R M) :
            (a : M) → M)
          x_1 :
        M)
⊢ HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (n • r)
      (AlgHom.toLinearMap (Algebra.lsmul R R M)) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) n : R)
      (HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
        (AlgHom.toLinearMap (Algebra.lsmul R R M)))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
n : R
r : A
x : B
x_1 : M
⊢ Eq (α := M)
    ((((HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) (n • r)
                  (AlgHom.toLinearMap (Algebra.lsmul R R M)) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)
    ((((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) n : R)
                  (HSMul.hSMul (β := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) B (Module.End R M)) r
                    (AlgHom.toLinearMap (Algebra.lsmul R R M))) :
                (a : B) → Module.End R M)
              x :
            Module.End R M) :
          (a : M) → M)
        x_1 :
      M)

Tactic:
simp only [RingHom.id_apply, LinearMap.smul_apply, smul_assoc]

Premises used: RingHom.id_apply, smul_assoc, LinearMap.smul_apply
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
a : A
b : B
m : M
⊢ (((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m = a • b • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (x * y) • m = x • y • m

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

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_1 : (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)
refine_2 : ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)
refine_3 :
  ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m
⊢ (x * y) • m = x • y • m

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)

Tactic:
TensorProduct.induction_on y ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_1 : HMul.hMul (α := A ⊗[R] B) 0 0 • m = HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) 0 m)
refine_1₁ :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) 0 (x ⊗ₜ[R] y) • m =
      HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m)
refine_1₂ :
  ∀ (x y : A ⊗[R] B),
    (0 * x) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (x • m) →
      (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m) →
        (0 * (x + y)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((x + y) • m)
⊢ (0 * y) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (y • m)

Tactic:
refine TensorProduct.induction_on y ?_ ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)

Tactic:
TensorProduct.induction_on y ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_2 :
  ∀ (x : A) (y : B),
    HMul.hMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) 0 • m =
      HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (HSMul.hSMul (α := A ⊗[R] B) 0 m)
refine_2₁ :
  ∀ (x : A) (y : B) (x_1 : A) (y_1 : B),
    HMul.hMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) (x ⊗ₜ[R] y) • m =
      HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) (HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m)
refine_2₂ :
  ∀ (x y : A ⊗[R] B),
    (∀ (x_1 : A) (y : B), (x_1 ⊗ₜ[R] y * x) • m = HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y) (x • m)) →
      (∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)) →
        ∀ (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * (x + y)) • m = HSMul.hSMul (α := A ⊗[R] B) (x_1 ⊗ₜ[R] y_1) ((x + y) • m)
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y_1) (y • m)

Tactic:
refine TensorProduct.induction_on y ?_ ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m

Tactic:
TensorProduct.induction_on y ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
refine_3 :
  ∀ (x y : A ⊗[R] B),
    (x * 0) • m = x • HSMul.hSMul (α := A ⊗[R] B) 0 m →
      (y * 0) • m = y • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((x + y) * 0) • m = (x + y) • HSMul.hSMul (α := A ⊗[R] B) 0 m
refine_3₁ :
  ∀ (x : A) (y : B) (x_1 y_1 : A ⊗[R] B),
    (x_1 * x ⊗ₜ[R] y) • m = x_1 • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m →
      (y_1 * x ⊗ₜ[R] y) • m = y_1 • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m →
        ((x_1 + y_1) * x ⊗ₜ[R] y) • m = (x_1 + y_1) • HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) m
refine_3₂ :
  ∀ (x y : A ⊗[R] B),
    (∀ (x_1 y : A ⊗[R] B),
        (x_1 * x) • m = x_1 • x • m → (y * x) • m = y • x • m → ((x_1 + y) * x) • m = (x_1 + y) • x • m) →
      (∀ (x y_1 : A ⊗[R] B),
          (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m) →
        ∀ (x_1 y_1 : A ⊗[R] B),
          (x_1 * (x + y)) • m = x_1 • (x + y) • m →
            (y_1 * (x + y)) • m = y_1 • (x + y) • m → ((x_1 + y_1) * (x + y)) • m = (x_1 + y_1) • (x + y) • m
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m

Tactic:
refine TensorProduct.induction_on y ?_ ?_ ?_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ HMul.hMul (α := A ⊗[R] B) 0 0 • m = HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) 0 m)

Tactic:
simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, MulZeroClass.mul_zero, HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
⊢ HMul.hMul (α := A ⊗[R] B) 0 (a ⊗ₜ[R] b) • m =
    HSMul.hSMul (α := A ⊗[R] B) 0 (HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m)

Tactic:
simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, MulZeroClass.zero_mul, map_zero, HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
refine_1 :
  (0 * z) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (z • m) →
    (0 * w) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (w • m) →
      (0 * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((z + w) • m)
⊢ (0 * z) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (z • m) →
    (0 * w) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (w • m) →
      (0 * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((z + w) • m)

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
h : (0 * z) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (z • m)
refine_1 :
  (0 * w) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (w • m) → (0 * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((z + w) • m)
⊢ (0 * w) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (w • m) → (0 * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((z + w) • m)

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
h : (0 * z) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (z • m)
h_1 : (0 * w) • m = HSMul.hSMul (α := A ⊗[R] B) 0 (w • m)
⊢ (0 * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) 0 ((z + w) • m)

Tactic:
simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, MulZeroClass.zero_mul, map_zero, HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
⊢ HMul.hMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) 0 • m =
    HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) (HSMul.hSMul (α := A ⊗[R] B) 0 m)

Tactic:
simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, MulZeroClass.mul_zero, HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a₁ : A
b₁ : B
a₂ : A
b₂ : B
refine_2 :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((a₂ * a₁) ⊗ₜ[R] (b₂ * b₁)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a₂ ⊗ₜ[R] b₂) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a₁ ⊗ₜ[R] b₁) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
⊢ HMul.hMul (α := A ⊗[R] B) (a₂ ⊗ₜ[R] b₂) (a₁ ⊗ₜ[R] b₁) • m =
    HSMul.hSMul (α := A ⊗[R] B) (a₂ ⊗ₜ[R] b₂) (HSMul.hSMul (α := A ⊗[R] B) (a₁ ⊗ₜ[R] b₁) m)

Tactic:
simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a₁ : A
b₁ : B
a₂ : A
b₂ : B
⊢ Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((a₂ * a₁) ⊗ₜ[R] (b₂ * b₁)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a₂ ⊗ₜ[R] b₂) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a₁ ⊗ₜ[R] b₁) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)

Tactic:
simp only [moduleAux_apply, mul_smul, smul_comm a₁ b₂]

Premises used: SMulCommClass.smul_comm, TensorProduct.Algebra.moduleAux_apply, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * z) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (z • m)
hw : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * w) • m = HSMul.hSMul (α := A ⊗[R] B) (x ⊗ₜ[R] y) (w • m)
a : A
b : B
refine_2 :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b * (z + w)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
⊢ (a ⊗ₜ[R] b * (z + w)) • m = HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) ((z + w) • m)

Tactic:
simp only [(· • ·)] at hz hw ⊢

Premises used: HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz :
  ∀ (x : A) (y : B),
    Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (x ⊗ₜ[R] y * z) : M →ₗ[R] M) : (a : M) → M) m : M)
      ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (x ⊗ₜ[R] y) : M →ₗ[R] M) : (a : M) → M)
          ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) z : M →ₗ[R] M) : (a : M) → M) m : M) :
        M)
hw :
  ∀ (x : A) (y : B),
    Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (x ⊗ₜ[R] y * w) : M →ₗ[R] M) : (a : M) → M) m : M)
      ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (x ⊗ₜ[R] y) : M →ₗ[R] M) : (a : M) → M)
          ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) w : M →ₗ[R] M) : (a : M) → M) m : M) :
        M)
a : A
b : B
⊢ Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b * (z + w)) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)

Tactic:
simp only [moduleAux_apply, mul_add, map_add,
        LinearMap.add_apply, moduleAux_apply, hz, hw]

Premises used: LinearMap.add_apply, map_add, mul_add, TensorProduct.Algebra.moduleAux_apply
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
refine_3 :
  (z * 0) • m = z • HSMul.hSMul (α := A ⊗[R] B) 0 m →
    (w * 0) • m = w • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((z + w) * 0) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) 0 m
⊢ (z * 0) • m = z • HSMul.hSMul (α := A ⊗[R] B) 0 m →
    (w * 0) • m = w • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((z + w) * 0) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) 0 m

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
h : (z * 0) • m = z • HSMul.hSMul (α := A ⊗[R] B) 0 m
refine_3 :
  (w * 0) • m = w • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((z + w) * 0) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) 0 m
⊢ (w * 0) • m = w • HSMul.hSMul (α := A ⊗[R] B) 0 m → ((z + w) * 0) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) 0 m

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
h : (z * 0) • m = z • HSMul.hSMul (α := A ⊗[R] B) 0 m
h_1 : (w * 0) • m = w • HSMul.hSMul (α := A ⊗[R] B) 0 m
⊢ ((z + w) * 0) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) 0 m

Tactic:
simp only [(· • ·), mul_zero, map_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, map_zero, MulZeroClass.mul_zero, HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz : (z * a ⊗ₜ[R] b) • m = z • HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m
hw : (w * a ⊗ₜ[R] b) • m = w • HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m
refine_3 :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((z + w) * a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
⊢ ((z + w) * a ⊗ₜ[R] b) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m

Tactic:
simp only [(· • ·)] at hz hw ⊢

Premises used: HSMul.hSMul
-- Module: Mathlib.RingTheory.TensorProduct.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z * a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) z : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
hw :
  Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (w * a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) w : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)
⊢ Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((z + w) * a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M)
    ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M)
        ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M) :
      M)

Tactic:
simp only [map_add, add_mul, LinearMap.add_apply, hz, hw]

Premises used: add_mul, LinearMap.add_apply, map_add