case mp
F : Type ?u.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup s f → ∃ b, b ∈ s ∧ a ≤ f b

case mpr
F : Type ?u.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b, b ∈ s ∧ a ≤ f b) → a ≤ sup s f
F : Type ?u.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ a ≤ sup s f ↔ ∃ b, b ∈ s ∧ a ≤ f b
apply Iff.intro
case mp.cons
F : Type ?u.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < 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.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < 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, le_sup_iff]
no goals
case mp.cons
F : Type ?u.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < 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, hle⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hle⟩
no goals
case mpr
F : Type ?u.208752
α : Type u_1
β : Type ?u.208758
γ : Type ?u.208761
ι : Type u_2
κ : Type ?u.208767
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b, b ∈ s ∧ a ≤ f b) → a ≤ sup s f
exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)