case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
⊢ Set.Nonempty ∅ → ∃ a, a ∈ ∅ ∧ ∀ (a' : α), a' ∈ ∅ → f a ≤ f a' → f a = f a'

case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
⊢ ∀ {a : α} {s : Set α},
    ¬a ∈ s →
      Set.Finite s →
        (Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a') →
          Set.Nonempty (insert a s) →
            ∃ a_5, a_5 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_5 ≤ f a' → f a_5 = f a'
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
⊢ Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
refine' h.induction_on _ _
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
⊢ ∀ {a : α} {s : Set α},
    ¬a ∈ s →
      Set.Finite s →
        (Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a') →
          Set.Nonempty (insert a s) →
            ∃ a_5, a_5 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_5 ≤ f a' → f a_5 = f a'
intro a s his _ ih _
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : s = ∅
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'

case refine'_2.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : Set.Nonempty s
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
cases' s.eq_empty_or_nonempty with h h
case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
case refine'_2.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : Set.Nonempty s
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
rcases ih h with ⟨b, hb, ih⟩
case pos
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'

case neg
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
by_cases h : f b ≤ f a
no goals
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s : Set α
h : Set.Finite s
⊢ Set.Nonempty ∅ → ∃ a, a ∈ ∅ ∧ ∀ (a' : α), a' ∈ ∅ → f a ≤ f a' → f a = f a'
exact fun h => absurd h not_nonempty_empty
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : s = ∅
⊢ a ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a ≤ f a' → f a = f a'
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : s = ∅
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
use a
no goals
case refine'_2.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h : s = ∅
⊢ a ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a ≤ f a' → f a = f a'
simp [h]
case pos
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
⊢ f c ≤ f a
case pos
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
refine' ⟨a, Set.mem_insert _ _, fun c hc hac => le_antisymm hac _⟩
case pos.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
s : Set α
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
c : α
his : ¬c ∈ s
a✝ : Set.Nonempty (insert c s)
h : f b ≤ f c
hc : c ∈ insert c s
hac : f c ≤ f c
⊢ f c ≤ f c

case pos.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
hcs : c ∈ s
⊢ f c ≤ f a
case pos
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
⊢ f c ≤ f a
rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
no goals
case pos.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
s : Set α
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
c : α
his : ¬c ∈ s
a✝ : Set.Nonempty (insert c s)
h : f b ≤ f c
hc : c ∈ insert c s
hac : f c ≤ f c
⊢ f c ≤ f c
rfl
no goals
case pos.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : f b ≤ f a
c : α
hc : c ∈ insert a s
hac : f a ≤ f c
hcs : c ∈ s
⊢ f c ≤ f a
rwa [← ih c hcs (le_trans h hac)]
case neg
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
⊢ f b = f c
case neg
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
⊢ ∃ a_1, a_1 ∈ insert a s ∧ ∀ (a' : α), a' ∈ insert a s → f a_1 ≤ f a' → f a_1 = f a'
refine' ⟨b, Set.mem_insert_of_mem _ hb, fun c hc hbc => _⟩
case neg.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
s : Set α
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
c : α
hbc : f b ≤ f c
his : ¬c ∈ s
a✝ : Set.Nonempty (insert c s)
h : ¬f b ≤ f c
hc : c ∈ insert c s
⊢ f b = f c

case neg.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
hcs : c ∈ s
⊢ f b = f c
case neg
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
⊢ f b = f c
rcases Set.mem_insert_iff.1 hc with (rfl | hcs)
no goals
case neg.inl
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
s : Set α
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
c : α
hbc : f b ≤ f c
his : ¬c ∈ s
a✝ : Set.Nonempty (insert c s)
h : ¬f b ≤ f c
hc : c ∈ insert c s
⊢ f b = f c
exact (h hbc).elim
no goals
case neg.inr
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : PartialOrder β
f : α → β
s✝ : Set α
h✝¹ : Set.Finite s✝
a : α
s : Set α
his : ¬a ∈ s
a✝¹ : Set.Finite s
ih✝ : Set.Nonempty s → ∃ a, a ∈ s ∧ ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a'
a✝ : Set.Nonempty (insert a s)
h✝ : Set.Nonempty s
b : α
hb : b ∈ s
ih : ∀ (a' : α), a' ∈ s → f b ≤ f a' → f b = f a'
h : ¬f b ≤ f a
c : α
hc : c ∈ insert a s
hbc : f b ≤ f c
hcs : c ∈ s
⊢ f b = f c
exact ih c hcs hbc