F : Type ?u.323869
α : Type u_1
β : Type ?u.323875
γ : Type ?u.323878
ι : Type ?u.323881
κ : Type ?u.323884
inst✝ : LinearOrder α
a : α
⊢ Finset.min (insert a ∅) = ↑a
F : Type ?u.323869
α : Type u_1
β : Type ?u.323875
γ : Type ?u.323878
ι : Type ?u.323881
κ : Type ?u.323884
inst✝ : LinearOrder α
a : α
⊢ Finset.min {a} = ↑a
rw [← insert_emptyc_eq]
no goals
F : Type ?u.323869
α : Type u_1
β : Type ?u.323875
γ : Type ?u.323878
ι : Type ?u.323881
κ : Type ?u.323884
inst✝ : LinearOrder α
a : α
⊢ Finset.min (insert a ∅) = ↑a
exact min_insert