case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j

case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j
by_cases h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
case pos.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
no goals
case pos.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ j, IsLUB (Iio i) j
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ i ∈ lowerBounds (upperBounds (Iio i))
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∃ j, IsLUB (Iio i) j
refine' ⟨i, fun j hj => le_of_lt hj, _⟩
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ i ∈ lowerBounds (upperBounds (Iio i))
rw [mem_lowerBounds]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ False
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
⊢ ∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
by_contra h
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ False
refine' h_exists_lt _
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ∃ x, x ∈ upperBounds (Iio i) ∧ x < i
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ¬∀ (x : γ), x ∈ upperBounds (Iio i) → i ≤ x
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
push_neg at h
no goals
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
a b : α
inst✝ : LinearOrder γ
i : γ
h_exists_lt : ¬∃ j, j ∈ upperBounds (Iio i) ∧ j < i
h : ∃ x, x ∈ upperBounds (Iio i) ∧ x < i
⊢ ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
exact h