case intro
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
h : Finset.Nonempty s
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
obtain ⟨c, hcs : c ∈ s⟩ := h
case intro
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
case intro
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
have : WellFounded (@LT.lt { x // x ∈ s } _) := Finite.wellFounded_of_trans_of_irrefl _
case intro.intro.mk.intro
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
m : α
hms : m ∈ s
H : ∀ (x : { x // x ∈ s }), x ∈ Set.univ → ¬x < { val := m, property := hms }
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
case intro
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min Set.univ ⟨⟨c, hcs⟩, trivial⟩
no goals
case intro.intro.mk.intro
α✝ : Type ?u.64966
β : Type ?u.64969
γ : Type ?u.64972
α : Type u_1
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
m : α
hms : m ∈ s
H : ∀ (x : { x // x ∈ s }), x ∈ Set.univ → ¬x < { val := m, property := hms }
⊢ ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬x < m
exact ⟨m, hms, fun x hx hxm => H ⟨x, hx⟩ trivial hxm⟩