Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁵ : CommSemiring R
inst✝⁴⁴ : CommSemiring R₂
inst✝⁴³ : CommSemiring R₃
inst✝⁴² : Monoid R'
inst✝⁴¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁰ : AddCommMonoid M
inst✝³⁹ : AddCommMonoid N
inst✝³⁸ : AddCommMonoid P
inst✝³⁷ : AddCommMonoid Q
inst✝³⁶ : AddCommMonoid S
inst✝³⁵ : AddCommMonoid P'
inst✝³⁴ : AddCommMonoid Q'
inst✝³³ : AddCommMonoid M₂
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid P₂
inst✝³⁰ : AddCommMonoid Q₂
inst✝²⁹ : AddCommMonoid M₃
inst✝²⁸ : AddCommMonoid N₃
inst✝²⁷ : AddCommMonoid P₃
inst✝²⁶ : AddCommMonoid Q₃
inst✝²⁵ : DistribMulAction R' M
inst✝²⁴ : Module R'' M
inst✝²³ : Module R M
inst✝²² : Module R N
inst✝²¹ : Module R S
inst✝²⁰ : Module R P'
inst✝¹⁹ : Module R Q'
inst✝¹⁸ : Module R₂ M₂
inst✝¹⁷ : Module R₂ N₂
inst✝¹⁶ : Module R₂ P₂
inst✝¹⁵ : Module R₂ Q₂
inst✝¹⁴ : Module R₃ M₃
inst✝¹³ : Module R₃ N₃
inst✝¹² : Module R₃ P₃
inst✝¹¹ : Module R₃ Q₃
inst✝¹⁰ : SMulCommClass R R' M
inst✝⁹ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁸ : Monoid R'₂
inst✝⁷ : DistribMulAction R'₂ M
inst✝⁶ : SMulCommClass R R'₂ M
inst✝⁵ : SMul R'₂ R'
inst✝⁴ : DistribMulAction R'₂ N
inst✝³ : DistribMulAction R' N
inst✝² : CompatibleSMul R R'₂ M N
inst✝¹ : CompatibleSMul R R' M N
inst✝ : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x✝ x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)

Tactic:
smul_add,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁵ : CommSemiring R
inst✝⁴⁴ : CommSemiring R₂
inst✝⁴³ : CommSemiring R₃
inst✝⁴² : Monoid R'
inst✝⁴¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁰ : AddCommMonoid M
inst✝³⁹ : AddCommMonoid N
inst✝³⁸ : AddCommMonoid P
inst✝³⁷ : AddCommMonoid Q
inst✝³⁶ : AddCommMonoid S
inst✝³⁵ : AddCommMonoid P'
inst✝³⁴ : AddCommMonoid Q'
inst✝³³ : AddCommMonoid M₂
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid P₂
inst✝³⁰ : AddCommMonoid Q₂
inst✝²⁹ : AddCommMonoid M₃
inst✝²⁸ : AddCommMonoid N₃
inst✝²⁷ : AddCommMonoid P₃
inst✝²⁶ : AddCommMonoid Q₃
inst✝²⁵ : DistribMulAction R' M
inst✝²⁴ : Module R'' M
inst✝²³ : Module R M
inst✝²² : Module R N
inst✝²¹ : Module R S
inst✝²⁰ : Module R P'
inst✝¹⁹ : Module R Q'
inst✝¹⁸ : Module R₂ M₂
inst✝¹⁷ : Module R₂ N₂
inst✝¹⁶ : Module R₂ P₂
inst✝¹⁵ : Module R₂ Q₂
inst✝¹⁴ : Module R₃ M₃
inst✝¹³ : Module R₃ N₃
inst✝¹² : Module R₃ P₃
inst✝¹¹ : Module R₃ Q₃
inst✝¹⁰ : SMulCommClass R R' M
inst✝⁹ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁸ : Monoid R'₂
inst✝⁷ : DistribMulAction R'₂ M
inst✝⁶ : SMulCommClass R R'₂ M
inst✝⁵ : SMul R'₂ R'
inst✝⁴ : DistribMulAction R'₂ N
inst✝³ : DistribMulAction R' N
inst✝² : CompatibleSMul R R'₂ M N
inst✝¹ : CompatibleSMul R R' M N
inst✝ : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x✝ x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
⊢ (s • r) • x + (s • r) • y = s • r • (x + y)