case h
α : Type u_1
β : Type ?u.72334
γ : Type ?u.72337
ι : Sort ?u.72340
π : α → Type ?u.72345
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ piecewise univ f g i = f i
α : Type u_1
β : Type ?u.72334
γ : Type ?u.72337
ι : Sort ?u.72340
π : α → Type ?u.72345
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
⊢ piecewise univ f g = f
ext i
no goals
case h
α : Type u_1
β : Type ?u.72334
γ : Type ?u.72337
ι : Sort ?u.72340
π : α → Type ?u.72345
δ : α → Sort u_2
s : Set α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ piecewise univ f g i = f i
simp [piecewise]