case h
α : Type u_1
β : Type ?u.94382
γ : Type ?u.94385
ι : Sort ?u.94388
π : α → Type ?u.94393
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ piecewise s f f x = f x
α : Type u_1
β : Type ?u.94382
γ : Type ?u.94385
ι : Sort ?u.94388
π : α → Type ?u.94393
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
⊢ piecewise s f f = f
ext x
no goals
case h
α : Type u_1
β : Type ?u.94382
γ : Type ?u.94385
ι : Sort ?u.94388
π : α → Type ?u.94393
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
⊢ piecewise s f f x = f x
by_cases hx : x ∈ s <;> simp [hx]