awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_sSup' hs

Premises used: WithTop.isLUB_sSup'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
left : sInf s ∈ lowerBounds s
right : sInf s ∈ upperBounds (lowerBounds s)
⊢ IsGLB s (sInf s)

Tactic:
constructor
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
left : (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s
⊢ (if s ⊆ {⊤} ∨ ¬BddBelow s then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s

Tactic:
simp only [hs, not_true_eq_false, or_false]

Premises used: not_true_eq_false, or_false
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
pos : ∀ (h : s ⊆ {⊤}), ⊤ ∈ lowerBounds s
neg : ∀ (h : ¬s ⊆ {⊤}), (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ lowerBounds s
⊢ (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s

Tactic:
split_ifs with h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
ha : a ∈ s
⊢ ⊤ ≤ a

Tactic:
top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))

Premises used: Iff.mpr, Set.mem_singleton_iff, top_le_iff, Iff.mp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
ha : a ∈ s
⊢ ⊤ ≤ a

Tactic:
exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))

Premises used: Iff.mpr, Set.mem_singleton_iff, top_le_iff, Iff.mp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ LE.le (α := WithTop β) (↑(sInf ((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 : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ LE.le (α := WithTop β) (↑(sInf ((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 : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some a

Tactic:
coe_le_coe.2 (csInf_le ?_ ha)

Premises used: Iff.mpr, WithTop.some, WithTop.coe_le_coe, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
neg : BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some a

Tactic:
refine coe_le_coe.2 (csInf_le ?_ ha)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
neg : ∀ (hb : none ∈ lowerBounds s), BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
neg₁ : ∀ (b : β) (hb : Option.some b ∈ lowerBounds s), BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ BddBelow (α := β) ((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 ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
neg : False
⊢ BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
exfalso
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
neg : s ⊆ {⊤}
⊢ False

Tactic:
apply h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
neg : ⊤ ≤ c
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} c

Tactic:
rw [mem_singleton_iff, ← top_le_iff]

Premises used: Set.mem_singleton_iff, top_le_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c

Tactic:
hb hc
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ ⊤ ≤ c

Tactic:
exact hb hc
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
h₁ : Membership.mem (γ := Set β) (lowerBounds ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) b
⊢ BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
use b
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
hc : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) c
⊢ b ≤ c

Tactic:
coe_le_coe.1 (hb hc)

Premises used: Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
hc : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) c
⊢ b ≤ c

Tactic:
exact coe_le_coe.1 (hb hc)

Premises used: Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
right :
  (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ upperBounds (lowerBounds s)
⊢ (if s ⊆ {⊤} ∨ ¬BddBelow s then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈
    upperBounds (lowerBounds s)

Tactic:
simp only [hs, not_true_eq_false, or_false]

Premises used: not_true_eq_false, or_false
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
pos : ∀ (h : s ⊆ {⊤}), ⊤ ∈ upperBounds (lowerBounds s)
neg : ∀ (h : ¬s ⊆ {⊤}), (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ upperBounds (lowerBounds s)
⊢ (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ upperBounds (lowerBounds s)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
pos : a ∈ lowerBounds s → a ≤ ⊤
⊢ a ∈ lowerBounds s → a ≤ ⊤

Tactic:
_
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
h_1 : a ∈ lowerBounds s
⊢ a ≤ ⊤

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
a : WithTop β
h_1 : a ∈ lowerBounds 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 : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
neg : False
⊢ LE.le (α := WithTop β) none (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)

Tactic:
exfalso
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
neg : s ⊆ {⊤}
⊢ False

Tactic:
apply h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} b

Tactic:
Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))

Premises used: Iff.mpr, Set.mem_singleton_iff, top_le_iff, Iff.mp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} b

Tactic:
exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))

Premises used: Iff.mpr, Set.mem_singleton_iff, top_le_iff, Iff.mp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : 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 : WithTop β)) ⁻¹' s)) : WithTop β)

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

Premises used: Iff.mpr, le_csInf, WithTop.some, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg : Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
neg₁ : ∀ (b : β), Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b → a ≤ b
⊢ Option.some a ≤ (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)

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

Premises used: Iff.mpr, le_csInf, WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅), s ⊆ {⊤}
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
contrapose! h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha_1 : Option.some a ∈ lowerBounds s
h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅
ha : none ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} none

Tactic:
mem_singleton ⊤

Premises used: Set.mem_singleton, Set.Mem, Top.top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha_1 : Option.some a ∈ lowerBounds s
h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅
ha : none ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} none

Tactic:
exact mem_singleton ⊤

Premises used: Set.mem_singleton, Top.top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a_1 : β
ha_1 : Option.some a_1 ∈ lowerBounds s
h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅
a : β
ha : Option.some a ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} (Option.some a)

Tactic:
(not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim

Premises used: Iff.mpr, Set.not_nonempty_iff_eq_empty, False.elim, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a_1 : β
ha_1 : Option.some a_1 ∈ lowerBounds s
h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅
a : β
ha : Option.some a ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} (Option.some a)

Tactic:
exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim

Premises used: Iff.mpr, Set.not_nonempty_iff_eq_empty, False.elim, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg neg₁ : ∀ (h : ¬s ⊆ {⊤}), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
neg₂ neg₃ neg₄ : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅), s ⊆ {⊤}
neg₅ :
  ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅) (ha : none ∈ s),
    Membership.mem (γ := Set (WithTop β)) {⊤} none
neg₆ neg₇ :
  ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅) (a : β) (ha : Option.some a ∈ s),
    Membership.mem (γ := Set (WithTop β)) {⊤} (Option.some a)
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)

Tactic:
classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim

Premises used: Set.mem_singleton, Top.top
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b
neg : (↑a : WithTop β) ≤ (↑b : WithTop β)
⊢ a ≤ b

Tactic:
rw [← coe_le_coe]

Premises used: WithTop.coe_le_coe
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b
⊢ (↑a : WithTop β) ≤ (↑b : WithTop β)

Tactic:
ha hb

Premises used: WithTop.some
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b
⊢ (↑a : WithTop β) ≤ (↑b : WithTop β)

Tactic:
exact ha hb
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
left : sInf s ∈ lowerBounds s
right right₁ : sInf s ∈ upperBounds (lowerBounds s)
⊢ IsGLB s (sInf s)

Tactic:
classical
  constructor
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
    · rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

Premises used: Iff.mpr, Set.mem_singleton, le_csInf, not_true_eq_false, Set.mem_singleton_iff, le_top, top_le_iff, or_false, WithTop.coe_le_coe, Top.top, ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
pos : ∀ (hs : BddBelow s), IsGLB s (sInf s)
neg : ∀ (hs : ¬BddBelow s), IsGLB s (sInf s)
⊢ IsGLB s (sInf s)

Tactic:
by_cases hs : BddBelow s

Premises used: BddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
isGLB_sInf' hs

Premises used: WithTop.isGLB_sInf'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
exact isGLB_sInf' hs

Premises used: WithTop.isGLB_sInf'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
isGLB_sInf' (OrderBot.bddBelow _)

Premises used: WithTop.isGLB_sInf', OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
exact isGLB_sInf' (OrderBot.bddBelow _)

Premises used: WithTop.isGLB_sInf', OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
rw : Eq (α := WithTop α) (sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) (⨆ a ∈ s, (↑a : WithTop α))
rw₁ rw₂ : Eq.{u_1 + 1} (α := WithTop α) (⨆ a ∈ s, (↑a : WithTop α)) (⨆ a ∈ s, (↑a : WithTop α))
⊢ (↑(sSup s) : WithTop α) = ⨆ a ∈ s, (↑a : WithTop α)

Tactic:
rw [coe_sSup' hb, sSup_image]

Premises used: WithTop.coe_sSup', sSup_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
rw : Eq (α := WithTop α) (sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) (⨅ a ∈ s, (↑a : WithTop α))
rw₁ rw₂ : Eq.{u_1 + 1} (α := WithTop α) (⨅ a ∈ s, (↑a : WithTop α)) (⨅ a ∈ s, (↑a : WithTop α))
⊢ (↑(sInf s) : WithTop α) = ⨅ a ∈ s, (↑a : WithTop α)

Tactic:
rw [coe_sInf' hs h's, sInf_image]

Premises used: sInf_image, WithTop.coe_sInf'
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddAbove s
⊢ f c ≤ sSup (f '' s)

Tactic:
le_csSup (map_bddAbove h_mono h_bdd) (mem_image_of_mem f hcs)

Premises used: Monotone.map_bddAbove, Set.mem_image_of_mem, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : s.Nonempty
B : α
hB : B ∈ upperBounds s
⊢ sSup (f '' s) ≤ f B

Tactic:
csSup_le (Nonempty.image f hs) (h_mono.mem_upperBounds_image hB)

Premises used: Set.Nonempty.image, Monotone.mem_upperBounds_image, csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
f' : αᵒᵈ → βᵒᵈ := f
⊢ sInf (f '' s) ≤ f c

Tactic:
le_csSup_image (α := αᵒᵈ) (β := βᵒᵈ)
    (show Monotone f' from fun x y hxy => h_mono hxy) hcs h_bdd

Premises used: Monotone.le_csSup_image, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
f' : αᵒᵈ → βᵒᵈ := f
⊢ sInf (f '' s) ≤ f c

Tactic:
exact le_csSup_image (α := αᵒᵈ) (β := βᵒᵈ)
    (show Monotone f' from fun x y hxy => h_mono hxy) hcs h_bdd

Premises used: Monotone.le_csSup_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : s.Nonempty
B : α
hB : B ∈ lowerBounds s
f' : αᵒᵈ → βᵒᵈ := f
⊢ f B ≤ sInf (f '' s)

Tactic:
csSup_image_le (α := αᵒᵈ) (β := βᵒᵈ)
    (show Monotone f' from fun x y hxy => h_mono hxy) hs hB

Premises used: Monotone.csSup_image_le, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : s.Nonempty
B : α
hB : B ∈ lowerBounds s
f' : αᵒᵈ → βᵒᵈ := f
⊢ f B ≤ sInf (f '' s)

Tactic:
exact csSup_image_le (α := αᵒᵈ) (β := βᵒᵈ)
    (show Monotone f' from fun x y hxy => h_mono hxy) hs hB

Premises used: Monotone.csSup_image_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
inl : ∀ (hst : ∅ ⊆ t) (h : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y), sInf (f '' ∅) = sInf (f '' t)
inr : ∀ (hs : s.Nonempty), sInf (f '' s) = sInf (f '' t)
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
obtain rfl | hs := Set.eq_empty_or_nonempty s

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y
⊢ t = ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem] using h

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y
inl :
  ∀ (ht : BddBelow (f '' ∅)) (hf : MonotoneOn f ∅) (hst : Subset.{u_1} (α := Set α) ∅ ∅)
    (h : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y),
    sInf (f '' ∅) = sInf (f '' ∅)
⊢ sInf (f '' ∅) = sInf (f '' t)

Tactic:
obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_notMem] using h

Premises used: rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
ht : BddBelow (f '' ∅)
hf : MonotoneOn f ∅
hst : Subset.{u_1} (α := Set α) ∅ ∅
h : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' ∅)

Tactic:
rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
ht₁ : BddBelow (f '' t)
hs₁ : (f '' s).Nonempty
⊢ sInf (f '' t) ≤ sInf (f '' s)

Tactic:
gcongr
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ BddBelow (f '' t)

Tactic:
ht
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ (f '' s).Nonempty

Tactic:
hs.image f

Premises used: Set.Nonempty.image