F : Type ?u.359873
α : Type u_1
β : Type ?u.359879
γ : Type ?u.359882
ι : Type ?u.359885
κ : Type ?u.359888
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsGreatest (insert a ↑s) (max a (max' s H))
F : Type ?u.359873
α : Type u_1
β : Type ?u.359879
γ : Type ?u.359882
ι : Type ?u.359885
κ : Type ?u.359888
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsGreatest (↑(insert a s)) (max (max' s H) a)
rw [coe_insert, max_comm]
no goals
F : Type ?u.359873
α : Type u_1
β : Type ?u.359879
γ : Type ?u.359882
ι : Type ?u.359885
κ : Type ?u.359888
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsGreatest (insert a ↑s) (max a (max' s H))
exact (isGreatest_max' _ _).insert _