α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ (b : WithTop α), b < ⊤ → ∃ i, b < ↑(f i)) ↔ ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (⨆ (x : ι), ↑(f x)) = ⊤ ↔ ¬BddAbove (range f)
rw [iSup_eq_top, not_bddAbove_iff]
case refine'_1
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (b : WithTop α), b < ⊤ → ∃ i, b < ↑(f i)
r : α
⊢ ∃ y, y ∈ range f ∧ r < y

case refine'_2
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ (b : WithTop α), b < ⊤ → ∃ i, b < ↑(f i)) ↔ ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
refine' ⟨fun hf r => _, fun hf a ha => _⟩
case refine'_1.intro
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (b : WithTop α), b < ⊤ → ∃ i, b < ↑(f i)
r : α
i : ι
hi : ↑r < ↑(f i)
⊢ ∃ y, y ∈ range f ∧ r < y
case refine'_1
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (b : WithTop α), b < ⊤ → ∃ i, b < ↑(f i)
r : α
⊢ ∃ y, y ∈ range f ∧ r < y
rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩
no goals
case refine'_1.intro
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (b : WithTop α), b < ⊤ → ∃ i, b < ↑(f i)
r : α
i : ι
hi : ↑r < ↑(f i)
⊢ ∃ y, y ∈ range f ∧ r < y
exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩
case refine'_2.intro.intro.intro
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : untop a (_ : a ≠ ⊤) < f i
⊢ ∃ i, a < ↑(f i)
case refine'_2
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)
rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩
no goals
case refine'_2.intro.intro.intro
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : untop a (_ : a ≠ ⊤) < f i
⊢ ∃ i, a < ↑(f i)
exact ⟨i, by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi⟩
no goals
α✝ : Type ?u.130874
β : Type ?u.130877
γ : Type ?u.130880
ι✝ : Sort ?u.130883
ι : Sort u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y, y ∈ range f ∧ x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : untop a (_ : a ≠ ⊤) < f i
⊢ a < ↑(f i)
simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi