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