no goals
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b c d : α
hf : Antitone f
⊢ f (max a b) = min (f a) (f b)
cases' le_total a b with h h <;> simp [h, hf h]