no goals
R : Type u_3
inst✝¹⁷ : CommSemiring R
R' : Type ?u.442286
inst✝¹⁶ : Monoid R'
R'' : Type ?u.442292
inst✝¹⁵ : Semiring R''
M : Type u_1
N : Type u_2
P✝ : Type ?u.442304
Q : Type ?u.442307
S : Type ?u.442310
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : AddCommMonoid P✝
inst✝¹¹ : AddCommMonoid Q
inst✝¹⁰ : AddCommMonoid S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P✝
inst✝⁶ : Module R Q
inst✝⁵ : Module R S
inst✝⁴ : DistribMulAction R' M
inst✝³ : Module R'' M
inst✝² : SMulCommClass R R' M
inst✝¹ : SMulCommClass R R'' M
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0
split_ifs <;> simp