case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
i' : ι
h : i = i'
⊢ ↑(single i (b₁ + b₂)) i' = ↑(single i b₁ + single i b₂) i'

case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
i' : ι
h : ¬i = i'
⊢ ↑(single i (b₁ + b₂)) i' = ↑(single i b₁ + single i b₂) i'
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
i' : ι
⊢ ↑(single i (b₁ + b₂)) i' = ↑(single i b₁ + single i b₂) i'
by_cases h : i = i'
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
⊢ ↑(single i (b₁ + b₂)) i = ↑(single i b₁ + single i b₂) i
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
i' : ι
h : i = i'
⊢ ↑(single i (b₁ + b₂)) i' = ↑(single i b₁ + single i b₂) i'
subst h
no goals
case pos
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
⊢ ↑(single i (b₁ + b₂)) i = ↑(single i b₁ + single i b₂) i
simp only [add_apply, single_eq_same]
no goals
case neg
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
b₁ b₂ : β i
i' : ι
h : ¬i = i'
⊢ ↑(single i (b₁ + b₂)) i' = ↑(single i b₁ + single i b₂) i'
simp only [add_apply, single_eq_of_ne h, zero_add]