awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
β : Type u_5
inst_2 : ConditionallyCompleteLattice β
f : α → β
hf : Monotone f
hs : s.Nonempty
⊢ f (sInf s) = sInf (f '' s)

Tactic:
(hf.map_isLeast (isLeast_csInf hs)).csInf_eq.symm

Premises used: isLeast_csInf, Monotone.map_isLeast, IsLeast.csInf_eq, Eq.symm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
inst_1 : OrderBot α
⊢ Eq.{u_1 + 1} (α := α) (sInf univ) ⊥

Tactic:
isLeast_univ.csInf_eq

Premises used: IsLeast.csInf_eq, isLeast_univ
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
⊢ Eq.{u_1 + 1} (α := α) (sSup ∅) ⊥

Tactic:
ConditionallyCompleteLinearOrderBot.csSup_empty

Premises used: ConditionallyCompleteLinearOrderBot.csSup_empty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
inl : ∀ (hs : BddAbove.{u_1} (α := α) ∅), IsLUB.{u_1} (α := α) ∅ (sSup ∅)
inr : ∀ (hne : s.Nonempty), IsLUB s (sSup s)
⊢ IsLUB s (sSup s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
hs : BddAbove.{u_1} (α := α) ∅
⊢ IsLUB.{u_1} (α := α) ∅ (sSup ∅)

Tactic:
simp only [csSup_empty, isLUB_empty]

Premises used: csSup_empty, isLUB_empty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
isLUB_csSup hne hs

Premises used: isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_csSup hne hs

Premises used: isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
a : α
⊢ sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a

Tactic:
isLUB_le_iff (isLUB_csSup' hs)

Premises used: Set.Mem, setOf, upperBounds, isLUB_le_iff, isLUB_csSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a ∈ upperBounds s
⊢ sSup s ≤ a

Tactic:
(csSup_le_iff' ⟨a, h⟩).2 h

Premises used: Iff.mpr, csSup_le_iff', Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hb : BddAbove s
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff' hb).not

Premises used: not_le, csSup_le_iff', Iff.not, exists_prop, not_forall₂
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : BddAbove s
⊢ a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

Tactic:
⟨fun h _ hb => le_trans h (csSup_le' hb), fun hb => hb _ fun _ => le_csSup h⟩

Premises used: csSup_le', Iff.intro, le_csSup, SupSet.sSup, le_trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
ne : s.Nonempty
⊢ a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

Tactic:
le_csInf_iff (OrderBot.bddBelow _) ne

Premises used: le_csInf_iff, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a ∈ s
⊢ sInf s ≤ a

Tactic:
csInf_le (OrderBot.bddBelow _) h

Premises used: OrderBot.bddBelow, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a < sSup s
contrapose! : ∀ (h : ∀ (b : α) (_ : b ∈ s), b ≤ a), sSup s ≤ a
⊢ ∃ b ∈ s, a < b

Tactic:
contrapose! h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ (b : α) (_ : b ∈ s), b ≤ a
⊢ sSup s ≤ a

Tactic:
csSup_le' h

Premises used: csSup_le'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ (b : α) (_ : b ∈ s), b ≤ a
⊢ sSup s ≤ a

Tactic:
exact csSup_le' h

Premises used: csSup_le'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
x : α
s : Set α
h : x < sInf s
⊢ x ∉ s

Tactic:
notMem_of_lt_csInf h (OrderBot.bddBelow s)

Premises used: notMem_of_lt_csInf, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : t.Nonempty
h₂ : t ⊆ s
⊢ sInf s ≤ sInf t

Tactic:
csInf_le_csInf (OrderBot.bddBelow s) h₁ h₂

Premises used: OrderBot.bddBelow, csInf_le_csInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
inl : ∀ (h₂ : ∅ ⊆ t), sSup ∅ ≤ sSup t
inr : ∀ (h : s.Nonempty), sSup s ≤ sSup t
⊢ sSup s ≤ sSup t

Tactic:
rcases eq_empty_or_nonempty s with rfl | h

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
inl : ⊥ ≤ sSup t
⊢ sSup ∅ ≤ sSup t

Tactic:
rw [csSup_empty]

Premises used: csSup_empty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ ⊥ ≤ sSup t

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t

Tactic:
csSup_le_csSup h₁ h h₂

Premises used: csSup_le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t

Tactic:
exact csSup_le_csSup h₁ h h₂

Premises used: csSup_le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
inl : ∀ (hs : BddAbove.{u_1} (α := α) ∅), sSup (∅ ∪ t) = max (sSup ∅) (sSup t)
inr : ∀ (hne : s.Nonempty), sSup (s ∪ t) = max (sSup s) (sSup t)
⊢ sSup (s ∪ t) = max (sSup s) (sSup t)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
t : Set α
ht : BddAbove t
hs : BddAbove.{u_1} (α := α) ∅
⊢ sSup (∅ ∪ t) = max (sSup ∅) (sSup t)

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : 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:
(isLUB_csSup' hs |>.union <| isLUB_csSup' ht).csSup_eq hne.inl

Premises used: IsLUB.union, Set.Nonempty.inl, IsLUB.csSup_eq, isLUB_csSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : 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:
exact (isLUB_csSup' hs |>.union <| isLUB_csSup' ht).csSup_eq hne.inl

Premises used: IsLUB.union, Set.Nonempty.inl, IsLUB.csSup_eq, isLUB_csSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s t : Set α
hs : BddAbove s
ht : BddAbove t
⊢ sSup (s ∩ t) ≤ min (sSup s) (sSup t)

Tactic:
csSup_le' fun _ hx ↦ le_inf (le_csSup hs hx.left) (le_csSup ht hx.right)

Premises used: csSup_le', le_inf, And.right, And.left, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hs : BddAbove s
⊢ sSup (insert a s) = max a (sSup s)

Tactic:
isLUB_csSup' hs |>.insert a |>.csSup_eq <| insert_nonempty a s

Premises used: Set.insert_nonempty, IsLUB.insert, IsLUB.csSup_eq, isLUB_csSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
left : sSup s ∈ upperBounds s
right : sSup s ∈ lowerBounds (upperBounds s)
⊢ IsLUB s (sSup s)

Tactic:
constructor
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ upperBounds s
pos₁ :
  ∀ (h₁ : ⊤ ∉ s) (h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)),
    (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ upperBounds s
neg : ∀ (h₁ : ⊤ ∉ s) (h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)), ⊤ ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    upperBounds s

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : WithTop β
pos : a ∈ s → a ≤ ⊤
⊢ a ∈ s → a ≤ ⊤

Tactic:
_
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : WithTop β
h : a ∈ s
⊢ a ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : WithTop β
h : a ∈ s
⊢ a ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
ha : none ∈ s
⊢ LE.le (α := WithTop β) none (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)

Tactic:
contradiction
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : β
ha : Option.some a ∈ s
pos : a ≤ sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ Option.some a ≤ (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)

Tactic:
apply coe_le_coe.2

Premises used: Iff.mpr, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ a ≤ sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
le_csSup h₂ ha

Premises used: le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ a ≤ sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
exact le_csSup h₂ ha

Premises used: le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : WithTop β
neg : a ∈ s → a ≤ ⊤
⊢ a ∈ s → a ≤ ⊤

Tactic:
_
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : WithTop β
h : a ∈ s
⊢ a ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
a : WithTop β
h : a ∈ s
⊢ a ≤ ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
pos : ∀ (h₁ : ⊤ ∈ s), ⊤ ∈ lowerBounds (upperBounds s)
pos₁ :
  ∀ (h₁ : ⊤ ∉ s) (h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)),
    (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ lowerBounds (upperBounds s)
neg : ∀ (h₁ : ⊤ ∉ s) (h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)), ⊤ ∈ lowerBounds (upperBounds s)
⊢ (if ⊤ ∈ s then ⊤
    else
      if BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) then
        (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
      else ⊤) ∈
    lowerBounds (upperBounds s)

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ LE.le.{u_5} (α := WithTop β) ⊤ none

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ LE.le.{u_5} (α := WithTop β) ⊤ none

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
False.elim (not_top_le_coe a (ha h₁))

Premises used: False.elim, WithTop.not_top_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
exact False.elim (not_top_le_coe a (ha h₁))

Premises used: False.elim, WithTop.not_top_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ LE.le (α := WithTop β) (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) none

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ LE.le (α := WithTop β) (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) none

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some b

Tactic:
coe_le_coe.2 (csSup_le ?_ ?_)

Premises used: Iff.mpr, WithTop.some, WithTop.coe_le_coe, csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
pos : Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
pos₁ : ∀ (b_1 : β), Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b_1 → b_1 ≤ b
⊢ (↑(sSup ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some b

Tactic:
refine coe_le_coe.2 (csSup_le ?_ ?_)

Premises used: Iff.mpr, WithTop.coe_le_coe, csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
pos : ∀ (hb : none ∈ s), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
pos₁ : ∀ (b : β) (hb : Option.some b ∈ s), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
rcases hs with ⟨⟨⟩ | b, hb⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb_1 : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
absurd hb h₁

Premises used: absurd
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb_1 : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
exact absurd hb h₁

Premises used: absurd
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b_1 : β
hb_1 : Option.some b_1 ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
⟨b, hb⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b_1 : β
hb_1 : Option.some b_1 ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
exact ⟨b, hb⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) a
⊢ a ≤ b

Tactic:
coe_le_coe.1 (hb ha)

Premises used: Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) a
⊢ a ≤ b

Tactic:
exact coe_le_coe.1 (hb ha)

Premises used: Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ LE.le.{u_5} (α := WithTop β) ⊤ none

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ LE.le.{u_5} (α := WithTop β) ⊤ none

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
neg : False
⊢ ⊤ ≤ Option.some b

Tactic:
exfalso
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
neg : BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ False

Tactic:
apply h₂
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
h : Membership.mem (γ := Set β) (upperBounds ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) b
⊢ BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
use b
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) a
⊢ a ≤ b

Tactic:
coe_le_coe.1 (hb ha)

Premises used: Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) a
⊢ a ≤ b

Tactic:
exact coe_le_coe.1 (hb ha)

Premises used: Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
left : sSup s ∈ upperBounds s
right right₁ : sSup s ∈ lowerBounds (upperBounds s)
⊢ IsLUB s (sSup s)

Tactic:
classical
  constructor
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

Premises used: Iff.mpr, le_rfl, le_top, WithTop.coe_le_coe, csSup_le, ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
inl : IsLUB.{u_1} (α := WithTop α) ∅ (sSup ∅)
inr : ∀ (hs : s.Nonempty), IsLUB s (sSup s)
⊢ IsLUB s (sSup s)

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
⊢ IsLUB.{u_1} (α := WithTop α) ∅ (sSup ∅)

Tactic:
simp [sSup]

Premises used: SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
isLUB_sSup' hs

Premises used: WithTop.isLUB_sSup'