α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ Set.piecewise (↑(insert j s)) f g = Set.piecewise (insert j ↑s) f g
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g = update (piecewise s f g) j (f j)
classical simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]
case h
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
x✝ : α
⊢ Set.piecewise (↑(insert j s)) f g x✝ = Set.piecewise (insert j ↑s) f g x✝
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ Set.piecewise (↑(insert j s)) f g = Set.piecewise (insert j ↑s) f g
ext
case h.e_s
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
x✝ : α
⊢ ↑(insert j s) = insert j ↑s
case h
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
x✝ : α
⊢ Set.piecewise (↑(insert j s)) f g x✝ = Set.piecewise (insert j ↑s) f g x✝
congr
no goals
case h.e_s
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
x✝ : α
⊢ ↑(insert j s) = insert j ↑s
simp
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ Set.piecewise (↑(insert j s)) f g = Set.piecewise (insert j ↑s) f g
α : Type u_1
β : Type ?u.298194
γ : Type ?u.298197
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g = update (piecewise s f g) j (f j)
simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]