case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
x y : Π₀ (i : ι), β i
s : Set ι
inst✝ : (i : ι) → Decidable (i ∈ s)
x✝ : ι
⊢ ↑(piecewise x y s) x✝ = Set.piecewise s (↑x) (↑y) x✝
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
x y : Π₀ (i : ι), β i
s : Set ι
inst✝ : (i : ι) → Decidable (i ∈ s)
⊢ ↑(piecewise x y s) = Set.piecewise s ↑x ↑y
ext
no goals
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
x y : Π₀ (i : ι), β i
s : Set ι
inst✝ : (i : ι) → Decidable (i ∈ s)
x✝ : ι
⊢ ↑(piecewise x y s) x✝ = Set.piecewise s (↑x) (↑y) x✝
apply piecewise_apply