α : Type u_1
β : Type ?u.69153
γ : Type ?u.69156
ι : Sort ?u.69159
inst✝¹ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
inst✝ : IsWellOrder α fun x x_1 => x < x_1
hs : Set.Nonempty s
⊢ IsLeast s (argminOn id (_ : WellFounded fun x x_1 => x < x_1) s hs)
α : Type u_1
β : Type ?u.69153
γ : Type ?u.69156
ι : Sort ?u.69159
inst✝¹ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
inst✝ : IsWellOrder α fun x x_1 => x < x_1
hs : Set.Nonempty s
⊢ IsLeast s (sInf s)
rw [sInf_eq_argmin_on hs]
no goals
α : Type u_1
β : Type ?u.69153
γ : Type ?u.69156
ι : Sort ?u.69159
inst✝¹ : ConditionallyCompleteLinearOrder α
s t : Set α
a b : α
inst✝ : IsWellOrder α fun x x_1 => x < x_1
hs : Set.Nonempty s
⊢ IsLeast s (argminOn id (_ : WellFounded fun x x_1 => x < x_1) s hs)
exact ⟨argminOn_mem _ _ _ _, fun a ha => argminOn_le id _ _ ha⟩