no goals
F : Type ?u.378979
α : Type u_1
β : Type ?u.378985
γ : Type ?u.378988
ι : Type ?u.378991
κ : Type ?u.378994
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ x : α
s : Finset α
h : ∃ y, y ∈ s ∧ x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ (fun x x_1 => x < x_1) x y
simpa
no goals
F : Type ?u.378979
α : Type u_1
β : Type ?u.378985
γ : Type ?u.378988
ι : Type ?u.378991
κ : Type ?u.378994
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ x : α
s : Finset α
h : ∃ y, y ∈ s ∧ x < y
Hne : Finset.Nonempty (filter ((fun x x_1 => x < x_1) x) s)
aux :
  min' (filter ((fun x x_1 => x < x_1) x) s) Hne ∈ s ∧
    (fun x x_1 => x < x_1) x (min' (filter ((fun x x_1 => x < x_1) x) s) Hne)
⊢ x < min' (filter ((fun x x_1 => x < x_1) x) s) Hne
simp
no goals
F : Type ?u.378979
α : Type u_1
β : Type ?u.378985
γ : Type ?u.378988
ι : Type ?u.378991
κ : Type ?u.378994
inst✝ : LinearOrder α
s✝ : Finset α
H : Finset.Nonempty s✝
x✝ x : α
s : Finset α
h : ∃ y, y ∈ s ∧ x < y
Hne : Finset.Nonempty (filter ((fun x x_1 => x < x_1) x) s)
aux :
  min' (filter ((fun x x_1 => x < x_1) x) s) Hne ∈ s ∧
    (fun x x_1 => x < x_1) x (min' (filter ((fun x x_1 => x < x_1) x) s) Hne)
z : α
hzs : z ∈ s
hz : x < z
⊢ (fun x x_1 => x < x_1) x z
simpa