α : Type u_1
β : Type ?u.308822
γ : Type ?u.308825
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
⊢ piecewise s (update f i v) (update g i v) = piecewise s f (update g i v)
α : Type u_1
β : Type ?u.308822
γ : Type ?u.308825
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
⊢ update (piecewise s f g) i v = piecewise s f (update g i v)
rw [update_piecewise]
α : Type u_1
β : Type ?u.308822
γ : Type ?u.308825
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
j : α
hj : j ∈ s
⊢ j ≠ i
α : Type u_1
β : Type ?u.308822
γ : Type ?u.308825
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
⊢ piecewise s (update f i v) (update g i v) = piecewise s f (update g i v)
refine' s.piecewise_congr (fun j hj => update_noteq _ _ _) fun _ _ => rfl
no goals
α : Type u_1
β : Type ?u.308822
γ : Type ?u.308825
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
j : α
hj : j ∈ s
⊢ j ≠ i
exact fun h => hi (h ▸ hj)