ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) { val := i, property := H } else 0) =
    c • if H : i ∈ s then x { val := i, property := H } else 0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ ↑(mk s (c • x)) i = ↑(c • mk s x) i
simp only [smul_apply, mk_apply]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) { val := i, property := H } else 0) =
    c • if H : i ∈ s then x { val := i, property := H } else 0
split_ifs <;> [rfl; rw [smul_zero]]