case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
f : Π₀ (i : ι), β i
b : β i
j i✝ : ι
⊢ ↑(update i f (↑f i)) i✝ = ↑f i✝
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
f : Π₀ (i : ι), β i
b : β i
j : ι
⊢ update i f (↑f i) = f
ext
no goals
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
f : Π₀ (i : ι), β i
b : β i
j i✝ : ι
⊢ ↑(update i f (↑f i)) i✝ = ↑f i✝
simp