α : Type u_2
β : Type ?u.97038
γ : Type ?u.97041
ι : Sort ?u.97044
π : α → Type ?u.97049
δ✝ : α → Sort ?u.97054
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_1
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
i : α
ht : i ∈ t
⊢ piecewise s f g i ∈ t' i
α : Type u_2
β : Type ?u.97038
γ : Type ?u.97041
ι : Sort ?u.97044
π : α → Type ?u.97049
δ✝ : α → Sort ?u.97054
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_1
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
⊢ piecewise s f g ∈ pi t t'
intro i ht
no goals
α : Type u_2
β : Type ?u.97038
γ : Type ?u.97041
ι : Sort ?u.97044
π : α → Type ?u.97049
δ✝ : α → Sort ?u.97054
s : Set α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_1
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ pi t t'
hg : g ∈ pi t t'
i : α
ht : i ∈ t
⊢ piecewise s f g i ∈ t' i
by_cases hs : i ∈ s <;> simp [hf i ht, hg i ht, hs]