ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ (if h : i✝ = i then (_ : i✝ = i) ▸ (c • x) else 0) = c • if h : i✝ = i then (_ : i✝ = i) ▸ x else 0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ ↑(single i✝ (c • x)) i = ↑(c • single i✝ x) i
simp only [smul_apply, single_apply]
case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : i✝ = i
⊢ (_ : i✝ = i) ▸ (c • x) = c • (_ : i✝ = i) ▸ x

case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : ¬i✝ = i
⊢ 0 = c • 0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ (if h : i✝ = i then (_ : i✝ = i) ▸ (c • x) else 0) = c • if h : i✝ = i then (_ : i✝ = i) ▸ x else 0
split_ifs with h
case inl.refl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i : ι
c : γ
x : β i
⊢ (_ : i = i) ▸ (c • x) = c • (_ : i = i) ▸ x
case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : i✝ = i
⊢ (_ : i✝ = i) ▸ (c • x) = c • (_ : i✝ = i) ▸ x
cases h
no goals
case inl.refl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i : ι
c : γ
x : β i
⊢ (_ : i = i) ▸ (c • x) = c • (_ : i = i) ▸ x
rfl
no goals
case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : ¬i✝ = i
⊢ 0 = c • 0
rw [smul_zero]