case h
α : Type u_1
β : Type ?u.22254
γ : Type ?u.22257
inst✝³ : Fintype α
s✝ t : Finset α
inst✝² : DecidableEq α
s : Finset α
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
δ : α → Sort u_2
f g : (i : α) → δ i
i : α
⊢ piecewise (sᶜ) f g i = piecewise s g f i
α : Type u_1
β : Type ?u.22254
γ : Type ?u.22257
inst✝³ : Fintype α
s✝ t : Finset α
inst✝² : DecidableEq α
s : Finset α
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
δ : α → Sort u_2
f g : (i : α) → δ i
⊢ piecewise (sᶜ) f g = piecewise s g f
ext i
no goals
case h
α : Type u_1
β : Type ?u.22254
γ : Type ?u.22257
inst✝³ : Fintype α
s✝ t : Finset α
inst✝² : DecidableEq α
s : Finset α
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
δ : α → Sort u_2
f g : (i : α) → δ i
i : α
⊢ piecewise (sᶜ) f g i = piecewise s g f i
simp [piecewise]