case h
α : Type u_1
β : Type ?u.294612
γ : Type ?u.294615
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ piecewise ∅ f g i = g i
α : Type u_1
β : Type ?u.294612
γ : Type ?u.294615
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
⊢ piecewise ∅ f g = g
ext i
no goals
case h
α : Type u_1
β : Type ?u.294612
γ : Type ?u.294615
δ : α → Sort u_2
s : Finset α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ piecewise ∅ f g i = g i
simp [piecewise]