no goals
C✝ : Type u
𝒞 : Category C✝
inst✝³ : MonoidalCategory C✝
C : Type u
inst✝² : Category C
inst✝¹ : MonoidalCategory C
U V W✝ X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ⊗ if h : P then g h else g' h) = if h : P then f ⊗ g h else f ⊗ g' h
split_ifs <;> rfl