Theorem: max_mem_of_mem (Sion/ForMathlib/Misc.lean)

State before:
α✝ : Type ?u.6414
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ max a b ∈ s
Tactic:
rw [max_def]
State after:
α✝ : Type ?u.6414
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then b else a) ∈ s

State before:
α✝ : Type ?u.6414
α : Type u_1
inst✝ : LinearOrder α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ (if a ≤ b then b else a) ∈ s
Tactic:
split_ifs <;> assumption
State after:
no goals