ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i i' : ι
b : β i
⊢ (if h : i' = i then (_ : i = i') ▸ b else OfNat.ofNat 0 i') = if h : i = i' then Eq.recOn h b else 0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i i' : ι
b : β i
⊢ ↑(single i b) i' = if h : i = i' then Eq.recOn h b else 0
rw [single_eq_pi_single, Pi.single, Function.update]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ i i' : ι
b : β i
⊢ (if h : i' = i then (_ : i = i') ▸ b else OfNat.ofNat 0 i') = if h : i = i' then Eq.recOn h b else 0
simp [@eq_comm _ i i']