case refine'_1
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f✝ : ι → α
a : α
f : ι → α
c : ι
⊢ ∃ i, i ∈ {c} ∧ sup' {c} (_ : Finset.Nonempty {c}) f = f i

case refine'_2
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
ih : ∃ i, i ∈ s ∧ sup' s hs f = f i
⊢ ∃ i, i ∈ cons c s hc ∧ sup' (cons c s hc) (_ : Finset.Nonempty (cons c s hc)) f = f i
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f✝ : ι → α
a : α
f : ι → α
⊢ ∃ i, i ∈ s ∧ sup' s H f = f i
refine' H.cons_induction (fun c => _) fun c s hc hs ih => _
no goals
case refine'_1
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s : Finset ι
H : Finset.Nonempty s
f✝ : ι → α
a : α
f : ι → α
c : ι
⊢ ∃ i, i ∈ {c} ∧ sup' {c} (_ : Finset.Nonempty {c}) f = f i
exact ⟨c, mem_singleton_self c, rfl⟩
case refine'_2.intro.intro
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
⊢ ∃ i, i ∈ cons c s hc ∧ sup' (cons c s hc) (_ : Finset.Nonempty (cons c s hc)) f = f i
case refine'_2
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
ih : ∃ i, i ∈ s ∧ sup' s hs f = f i
⊢ ∃ i, i ∈ cons c s hc ∧ sup' (cons c s hc) (_ : Finset.Nonempty (cons c s hc)) f = f i
rcases ih with ⟨b, hb, h'⟩
case refine'_2.intro.intro
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
case refine'_2.intro.intro
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
⊢ ∃ i, i ∈ cons c s hc ∧ sup' (cons c s hc) (_ : Finset.Nonempty (cons c s hc)) f = f i
rw [sup'_cons hs, h']
no goals
case refine'_2.intro.intro
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
cases le_total (f b) (f c) with
| inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
| inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩
no goals
case refine'_2.intro.intro.inl
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
h : f b ≤ f c
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
no goals
case refine'_2.intro.intro.inr
F : Type ?u.307909
α : Type u_2
β : Type ?u.307915
γ : Type ?u.307918
ι : Type u_1
κ : Type ?u.307924
inst✝ : LinearOrder α
s✝ : Finset ι
H : Finset.Nonempty s✝
f✝ : ι → α
a : α
f : ι → α
c : ι
s : Finset ι
hc : ¬c ∈ s
hs : Finset.Nonempty s
b : ι
hb : b ∈ s
h' : sup' s hs f = f b
h : f c ≤ f b
⊢ ∃ i, i ∈ cons c s hc ∧ f c ⊔ f b = f i
exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩