case mp
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup s f → ∃ b, b ∈ s ∧ a < f b

case mpr
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ a < f b) → a < sup s f
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < sup s f ↔ ∃ b, b ∈ s ∧ a < f b
apply Iff.intro
case mp.cons
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a < sup t f → ∃ b, b ∈ t ∧ a < f b
⊢ a < f c ∨ a < sup t f → ∃ b, b ∈ cons c t hc ∧ a < f b
case mp.cons
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a < sup t f → ∃ b, b ∈ t ∧ a < f b
⊢ a < sup (cons c t hc) f → ∃ b, b ∈ cons c t hc ∧ a < f b
rw [sup_cons, lt_sup_iff]
no goals
case mp.cons
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
c : ι
t : Finset ι
hc : ¬c ∈ t
ih : a < sup t f → ∃ b, b ∈ t ∧ a < f b
⊢ a < f c ∨ a < sup t f → ∃ b, b ∈ cons c t hc ∧ a < f b
exact fun
| Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
| Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
no goals
case mpr
F : Type ?u.212488
α : Type u_1
β : Type ?u.212494
γ : Type ?u.212497
ι : Type u_2
κ : Type ?u.212503
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (∃ b, b ∈ s ∧ a < f b) → a < sup s f
exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)