F : Type ?u.332825
α : Type u_1
β : Type ?u.332831
γ : Type ?u.332834
ι : Type ?u.332837
κ : Type ?u.332840
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ inf s WithTop.some = inf s (WithTop.some ∘ fun x => x)
F : Type ?u.332825
α : Type u_1
β : Type ?u.332831
γ : Type ?u.332834
ι : Type ?u.332837
κ : Type ?u.332840
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ Finset.min s = ↑(min' s H)
simp only [Finset.min, min', id_eq, coe_inf']
no goals
F : Type ?u.332825
α : Type u_1
β : Type ?u.332831
γ : Type ?u.332834
ι : Type ?u.332837
κ : Type ?u.332840
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
⊢ inf s WithTop.some = inf s (WithTop.some ∘ fun x => x)
rfl