mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup s ≤ sSup t

pp: case a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s

Tactic:
·

Goal state after:
case pos.a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup s ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
⊢ sSup t ≤ sSup s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : ¬(BddAbove s ∨ BddAbove t)
⊢ sSup s = sSup t

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : ¬(BddAbove s ∨ BddAbove t)
⊢ sSup s = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
⊢ sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
t : Set α
⊢ sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.Nonempty
⊢ sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)

pp: case inr.inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.Nonempty
⊢ sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i ↦ f i, x ≤ y

pp: case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i ↦ f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x

Tactic:
·

Goal state after:
case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i ↦ f i, x ≤ y
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i ↦ f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x

Tactic:
·

Goal state after:
case ht
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ y ∈ range fun i ↦ f i, ∃ x ∈ ⋃ i, Iic (f i), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a

pp: case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
ht : BddAbove t
hs : BddAbove ∅
⊢ sSup (∅ ∪ t) = max (sSup ∅) (sSup t)

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
hne : s.Nonempty
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
ht : BddAbove t
hs : BddAbove ∅
⊢ sSup (∅ ∪ t) = max (sSup ∅) (sSup t)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ upperBounds s

pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ lowerBounds (upperBounds s)

Tactic:
·

Goal state after:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ upperBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s

pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds s

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
·

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds s

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
·

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s))

pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ≤ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
·

Goal state after:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
·

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ lowerBounds (upperBounds s)

Tactic:
·

Goal state after:
case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ sSup s ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ lowerBounds (upperBounds s)

pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
·

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none

pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
·

Goal state after:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
·

Goal state after:
case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
·

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ≤ none

pp: case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ≤ Option.some b

Tactic:
·

Goal state after:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s)) ≤ none
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
·

Goal state after:
case pos.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

pp: case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
·

Goal state after:
case pos.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

Tactic:
·

Goal state after:
case pos.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
·

Goal state after:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
·

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ lowerBounds (upperBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ⊤ ≤ none

pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b

Tactic:
·

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ⊤ ≤ none
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b

Tactic:
·

Goal state after:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ⊤ ≤ Option.some b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
⊢ IsLUB ∅ (sSup ∅)

pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
⊢ IsLUB ∅ (sSup ∅)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ lowerBounds s

pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)

Tactic:
·

Goal state after:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ lowerBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s

Tactic:
·

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s

Tactic:
·

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ≤ none

pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ≤ Option.some a

Tactic:
·

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ≤ none
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' s)

pp: case neg.some.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' s)

Tactic:
·

Goal state after:
case neg.some.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)

Tactic:
·

Goal state after:
case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ sInf s ∈ upperBounds (lowerBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)

pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)

Tactic:
·

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)

Tactic:
·

Goal state after:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
·

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))