case h
α : Type u_1
β : Type ?u.305556
γ : Type ?u.305559
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
j : α
⊢ update (piecewise s f g) i v j = piecewise s (update f i v) (update g i v) j
α : Type u_1
β : Type ?u.305556
γ : Type ?u.305559
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
⊢ update (piecewise s f g) i v = piecewise s (update f i v) (update g i v)
ext j
no goals
case h
α : Type u_1
β : Type ?u.305556
γ : Type ?u.305559
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
j : α
⊢ update (piecewise s f g) i v j = piecewise s (update f i v) (update g i v) j
rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]