case intro.intro.intro.intro
F : Type ?u.344901
α : Type u_1
β : Type ?u.344907
γ : Type ?u.344910
ι : Type ?u.344913
κ : Type ?u.344916
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
h₂ : 1 < card s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ min' s (_ : Finset.Nonempty s) < max' s (_ : Finset.Nonempty s)
F : Type ?u.344901
α : Type u_1
β : Type ?u.344907
γ : Type ?u.344910
ι : Type ?u.344913
κ : Type ?u.344916
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
h₂ : 1 < card s
⊢ min' s (_ : Finset.Nonempty s) < max' s (_ : Finset.Nonempty s)
rcases one_lt_card.1 h₂ with ⟨a, ha, b, hb, hab⟩
no goals
case intro.intro.intro.intro
F : Type ?u.344901
α : Type u_1
β : Type ?u.344907
γ : Type ?u.344910
ι : Type ?u.344913
κ : Type ?u.344916
inst✝ : LinearOrder α
s : Finset α
H : Finset.Nonempty s
x : α
h₂ : 1 < card s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ min' s (_ : Finset.Nonempty s) < max' s (_ : Finset.Nonempty s)
exact s.min'_lt_max' ha hb hab