no goals
α : Type u_2
β : Type ?u.310085
γ : Type ?u.310088
δ✝ : α → Sort ?u.310093
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_1
inst✝ : (i : α) → Preorder (δ i)
f g f' g' : (i : α) → δ i
Hf : ∀ (x : α), x ∈ s → f x ≤ f' x
Hg : ∀ (x : α), ¬x ∈ s → g x ≤ g' x
x : α
⊢ piecewise s f g x ≤ piecewise s f' g' x
by_cases hx : x ∈ s <;> simp [hx, *]