F : Type ?u.361063
α : Type u_1
β : Type ?u.361069
γ : Type ?u.361072
ι : Type ?u.361075
κ : Type ?u.361078
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsLeast (insert a ↑s) (min a (min' s H))
F : Type ?u.361063
α : Type u_1
β : Type ?u.361069
γ : Type ?u.361072
ι : Type ?u.361075
κ : Type ?u.361078
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsLeast (↑(insert a s)) (min (min' s H) a)
rw [coe_insert, min_comm]
no goals
F : Type ?u.361063
α : Type u_1
β : Type ?u.361069
γ : Type ?u.361072
ι : Type ?u.361075
κ : Type ?u.361078
inst✝ : LinearOrder α
s✝ : Finset α
H✝ : Finset.Nonempty s✝
x a : α
s : Finset α
H : Finset.Nonempty s
⊢ IsLeast (insert a ↑s) (min a (min' s H))
exact (isLeast_min' _ _).insert _