F : Type ?u.312871
α : Type u_1
β : Type ?u.312877
γ : Type ?u.312880
ι : Type ?u.312883
κ : Type ?u.312886
inst✝ : LinearOrder α
a : α
⊢ Finset.max (insert a ∅) = ↑a
F : Type ?u.312871
α : Type u_1
β : Type ?u.312877
γ : Type ?u.312880
ι : Type ?u.312883
κ : Type ?u.312886
inst✝ : LinearOrder α
a : α
⊢ Finset.max {a} = ↑a
rw [← insert_emptyc_eq]
no goals
F : Type ?u.312871
α : Type u_1
β : Type ?u.312877
γ : Type ?u.312880
ι : Type ?u.312883
κ : Type ?u.312886
inst✝ : LinearOrder α
a : α
⊢ Finset.max (insert a ∅) = ↑a
exact max_insert