no goals
α : Type u_2
β : Type ?u.81703
γ : Type ?u.81706
ι : Sort ?u.81709
π : α → Type ?u.81714
δ✝ : α → Sort ?u.81719
s✝ : Set α
f g : (i : α) → δ✝ i
inst✝² : (j : α) → Decidable (j ∈ s✝)
δ : α → Type u_1
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ piecewise s f₁ f₂ ≤ piecewise s g₁ g₂
apply piecewise_le <;> intros <;> simp [*]