awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
pos : ∀ (hab : a = b), min a b = if a ≤ b then a else b
neg : ∀ (hab : ¬a = b), min a b = if a ≤ b then a else b
⊢ min a b = if a ≤ b then a else b

Tactic:
by_cases hab : a = b
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : a = b
⊢ min a b = if a ≤ b then a else b

Tactic:
simp [hab]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
neg : ∀ (h₁ : a ≤ b), min a b = if a ≤ b then a else b
neg₁ : ∀ (h₂ : b ≤ a), min a b = if a ≤ b then a else b
⊢ min a b = if a ≤ b then a else b

Tactic:
rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)

Premises used: ConditionallyCompleteLinearOrder.le_total
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₁ : a ≤ b
⊢ min a b = if a ≤ b then a else b

Tactic:
simp [h₁]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ min a b = if a ≤ b then a else b

Tactic:
simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

Premises used: le_antisymm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
pos : ∀ (hab : a = b), max a b = if a ≤ b then b else a
neg : ∀ (hab : ¬a = b), max a b = if a ≤ b then b else a
⊢ max a b = if a ≤ b then b else a

Tactic:
by_cases hab : a = b
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : a = b
⊢ max a b = if a ≤ b then b else a

Tactic:
simp [hab]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
neg : ∀ (h₁ : a ≤ b), max a b = if a ≤ b then b else a
neg₁ : ∀ (h₂ : b ≤ a), max a b = if a ≤ b then b else a
⊢ max a b = if a ≤ b then b else a

Tactic:
rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)

Premises used: ConditionallyCompleteLinearOrder.le_total
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₁ : a ≤ b
⊢ max a b = if a ≤ b then b else a

Tactic:
simp [h₁]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
h₂ : b ≤ a
⊢ max a b = if a ≤ b then b else a

Tactic:
simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]

Premises used: le_antisymm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hn : s.Nonempty
hb : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
ConditionallyCompleteLattice.isLUB_csSup _ hn hb

Premises used: ConditionallyCompleteLattice.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
h₁ : BddAbove s
h₂ : a ∈ s
⊢ a ≤ sSup s

Tactic:
(isLUB_csSup (nonempty_of_mem h₂) h₁).1 h₂

Premises used: And.left, Set.nonempty_of_mem, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
h₁ : s.Nonempty
h₂ : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a

Tactic:
(isLUB_csSup h₁ ⟨a, h₂⟩).2 h₂

Premises used: And.right, Exists.intro, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a b : α
hs : BddAbove s
hb : b ∈ s
h : a ≤ b
⊢ a ≤ sSup s

Tactic:
le_trans h (le_csSup hs hb)

Premises used: le_csSup, le_trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
ht : BddAbove t
hs : s.Nonempty
h : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
csSup_le hs fun _ ha => le_csSup ht (h ha)

Premises used: le_csSup, csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
ht : BddBelow t
hs : s.Nonempty
h : s ⊆ t
⊢ sInf t ≤ sInf s

Tactic:
le_csInf hs fun _ ha => csInf_le ht (h ha)

Premises used: le_csInf, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
h : BddAbove s
hs : s.Nonempty
⊢ a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

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

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

Tactic:
⟨fun h _ hb => le_trans (le_csInf hs hb) h, fun hb => hb _ fun _ => csInf_le h⟩

Premises used: le_csInf, Iff.intro, csInf_le, InfSet.sInf, le_trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
H : IsLUB s a
ne : s.Nonempty
⊢ sSup s = a

Tactic:
(isLUB_csSup ne ⟨a, H.1⟩).unique H

Premises used: IsLUB.unique, And.left, Exists.intro, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
hb : BddBelow s
ha : BddAbove s
⊢ s ⊆ Icc (sInf s) (sSup s)

Tactic:
fun _ hx => ⟨csInf_le hb hx, le_csSup ha hx⟩

Premises used: Set.Mem, setOf, Set.Subset, Set.Icc, And.intro, le_csSup, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
hb : BddAbove s
hs : s.Nonempty
⊢ sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

Tactic:
isLUB_le_iff (isLUB_csSup hs hb)

Premises used: Set.Mem, setOf, upperBounds, isLUB_le_iff, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
hb : BddBelow s
hs : s.Nonempty
⊢ a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

Tactic:
le_isGLB_iff (isGLB_csInf hs hb)

Premises used: lowerBounds, Set.Mem, setOf, isGLB_csInf, le_isGLB_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddBelow s
hs : s.Nonempty
⊢ sSup (lowerBounds s) = sInf s

Tactic:
(isLUB_csSup h <| hs.mono fun _ hx _ hy => hy hx).unique (isGLB_csInf hs h).isLUB

Premises used: Set.Nonempty.mono, IsGreatest.isLUB, isGLB_csInf, IsLUB.unique, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf (upperBounds s) = sSup s

Tactic:
(isGLB_csInf h <| hs.mono fun _ hx _ hy => hy hx).unique (isLUB_csSup hs h).isGLB

Premises used: IsLeast.isGLB, Set.Nonempty.mono, isGLB_csInf, isLUB_csSup, IsGLB.unique
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty β
f : β → α
hf : BddBelow (range f)
⊢ sSup (lowerBounds (range f)) = ⨅ (i : β), f i

Tactic:
csSup_lowerBounds_eq_csInf hf <| range_nonempty _

Premises used: iInf, csSup_lowerBounds_eq_csInf, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLattice α
inst_1 : Nonempty β
f : β → α
hf : BddAbove (range f)
⊢ sInf (upperBounds (range f)) = ⨆ (i : β), f i

Tactic:
csInf_upperBounds_eq_csSup hf <| range_nonempty _

Premises used: iSup, Set.range_nonempty, csInf_upperBounds_eq_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
x : α
s : Set α
h : x < sInf s
hs : BddBelow s
⊢ x ∉ s

Tactic:
fun hx => lt_irrefl _ (h.trans_le (csInf_le hs hx))

Premises used: lt_irrefl, LT.lt.trans_le, csInf_le, Not
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
x : α
s : Set α
h : sSup s < x
hs : BddAbove s
⊢ x ∉ s

Tactic:
notMem_of_lt_csInf (α := αᵒᵈ) h hs

Premises used: Set.Mem, notMem_of_lt_csInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
b : α
hs : s.Nonempty
H : ∀ a ∈ s, a ≤ b
H' : ∀ w < b, ∃ a ∈ s, w < a
⊢ sSup s = b

Tactic:
(eq_of_le_of_not_lt (csSup_le hs H)) fun hb =>
    let ⟨_, ha, ha'⟩ := H' _ hb
    lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha

Premises used: False, lt_irrefl, LT.lt.trans_le, Exists.intro, le_csSup, _private.0.csSup_eq_of_forall_le_of_forall_lt_exists_gt.match_1, eq_of_le_of_not_lt, csSup_le, SupSet.sSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
b : α
⊢ s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ)

Premises used: Set.Mem, csSup_eq_of_forall_le_of_forall_lt_exists_gt, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a b : α
hs : BddAbove s
ha : a ∈ s
h : b < a
⊢ b < sSup s

Tactic:
lt_of_lt_of_le h (le_csSup hs ha)

Premises used: le_csSup, lt_of_lt_of_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a b : α
⊢ BddBelow s → a ∈ s → a < b → sInf s < b

Tactic:
lt_csSup_of_lt (α := αᵒᵈ)

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, lt_csSup_of_lt, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
sne : s.Nonempty
tne : t.Nonempty
hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
⊢ (upperBounds s ∩ lowerBounds t).Nonempty

Tactic:
⟨sInf t, fun x hx => le_csInf tne <| hst x hx, fun _ hy => csInf_le (sne.mono hst) hy⟩

Premises used: le_csInf, Set.Nonempty.mono, Set.Nonempty, And.intro, Exists.intro, csInf_le, InfSet.sInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a b : α
⊢ sSup {a, b} = a ⊔ b

Tactic:
(@isLUB_pair _ _ a b).csSup_eq (insert_nonempty _ _)

Premises used: Set.insert_nonempty, isLUB_pair, IsLUB.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a b : α
⊢ sInf {a, b} = a ⊓ b

Tactic:
(@isGLB_pair _ _ a b).csInf_eq (insert_nonempty _ _)

Premises used: Set.insert_nonempty, isGLB_pair, IsGLB.csInf_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
ne : s.Nonempty
hb : BddBelow s
ha : BddAbove s
⊢ sInf s ≤ sSup s

Tactic:
isGLB_le_isLUB (isGLB_csInf ne hb) (isLUB_csSup ne ha) ne

Premises used: isGLB_csInf, isGLB_le_isLUB, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
h : (s ∩ t).Nonempty
hs : BddBelow s
ht : BddAbove t
⊢ sInf s ≤ sSup t

Tactic:
isGLB_le_isLUB_of_nonempty_inter h (isGLB_csInf h.left hs) (isLUB_csSup h.right ht)

Premises used: Set.Nonempty.right, isGLB_csInf, Set.Nonempty.left, isLUB_csSup, isGLB_le_isLUB_of_nonempty_inter
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
hs : BddAbove s
sne : s.Nonempty
ht : BddAbove t
tne : t.Nonempty
⊢ sSup (s ∪ t) = sSup s ⊔ sSup t

Tactic:
((isLUB_csSup sne hs).union (isLUB_csSup tne ht)).csSup_eq sne.inl

Premises used: IsLUB.union, Set.Nonempty.inl, IsLUB.csSup_eq, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
hs : BddBelow s
sne : s.Nonempty
ht : BddBelow t
tne : t.Nonempty
⊢ sInf (s ∪ t) = sInf s ⊓ sInf t

Tactic:
csSup_union (α := αᵒᵈ) hs sne ht tne

Premises used: OrderDual, csSup_union
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
hs : BddAbove s
ht : BddAbove t
hst : (s ∩ t).Nonempty
⊢ sSup (s ∩ t) ≤ sSup s ⊓ sSup t

Tactic:
(csSup_le hst) fun _ hx => le_inf (le_csSup hs hx.1) (le_csSup ht hx.2)

Premises used: le_inf, And.right, And.left, le_csSup, csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s t : Set α
⊢ BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t)

Tactic:
csSup_inter_le (α := αᵒᵈ)

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, csSup_inter_le, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
hs : BddAbove s
sne : s.Nonempty
⊢ sSup (insert a s) = a ⊔ sSup s

Tactic:
((isLUB_csSup sne 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_1
inst : ConditionallyCompleteLattice α
s : Set α
a : α
hs : BddBelow s
sne : s.Nonempty
⊢ sInf (insert a s) = a ⊓ sInf s

Tactic:
csSup_insert (α := αᵒᵈ) hs sne

Premises used: csSup_insert, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : DenselyOrdered α
h : a < b
⊢ sInf (Ioc a b) = a

Tactic:
(isGLB_Ioc h).csInf_eq (nonempty_Ioc.2 h)

Premises used: Iff.mpr, Set.nonempty_Ioc, IsGLB.csInf_eq, isGLB_Ioc
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a : α
inst_1 : NoMaxOrder α
inst_2 : DenselyOrdered α
w : α
hw : a < w
⊢ ∃ a_1 ∈ Ioi a, a_1 < w

Tactic:
simpa using exists_between hw

Premises used: exists_between
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : DenselyOrdered α
h : a < b
⊢ sInf (Ioo a b) = a

Tactic:
(isGLB_Ioo h).csInf_eq (nonempty_Ioo.2 h)

Premises used: Iff.mpr, isGLB_Ioo, Set.nonempty_Ioo, IsGLB.csInf_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : DenselyOrdered α
h : a < b
⊢ sSup (Ico a b) = b

Tactic:
(isLUB_Ico h).csSup_eq (nonempty_Ico.2 h)

Premises used: Iff.mpr, Set.nonempty_Ico, isLUB_Ico, IsLUB.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a : α
inst_1 : NoMinOrder α
inst_2 : DenselyOrdered α
w : α
hw : w < a
⊢ ∃ a_1 ∈ Iio a, w < a_1

Tactic:
simpa [and_comm] using exists_between hw

Premises used: exists_between, and_comm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : DenselyOrdered α
h : a < b
⊢ sSup (Ioo a b) = b

Tactic:
(isLUB_Ioo h).csSup_eq (nonempty_Ioo.2 h)

Premises used: Iff.mpr, Set.nonempty_Ioo, isLUB_Ioo, IsLUB.csSup_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
s : Set α
b : α
hs : s.Nonempty
h_is_ub : ∀ a ∈ s, a ≤ b
h_b_le_ub : ∀ (ub : α), (∀ a ∈ s, a ≤ ub) → b ≤ ub
⊢ sSup s = b

Tactic:
(csSup_le hs h_is_ub).antisymm ((h_b_le_ub _) fun _ => le_csSup ⟨b, h_is_ub⟩)

Premises used: LE.le.antisymm, Exists.intro, le_csSup, csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddAbove x
x_1 : ι
rw : IsLUB (eval (β := α) x_1 '' x) (sSup (eval (β := α) x_1 '' x))
⊢ IsLUB (eval (β := α) x_1 '' x) (sSup x x_1)

Tactic:
rw [sSup_apply_eq_sSup_image]

Premises used: sSup_apply_eq_sSup_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddAbove x
x_1 : ι
⊢ IsLUB (eval (β := α) x_1 '' x) (sSup (eval (β := α) x_1 '' x))

Tactic:
isLUB_csSup (image_nonempty.mpr hn) ((monotone_eval _).map_bddAbove hb)

Premises used: Iff.mpr, Set.image_nonempty, Function.monotone_eval, Monotone.map_bddAbove, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddAbove x
x_1 : ι
⊢ IsLUB (eval (β := α) x_1 '' x) (sSup (eval (β := α) x_1 '' x))

Tactic:
exact isLUB_csSup (image_nonempty.mpr hn) ((monotone_eval _).map_bddAbove hb)

Premises used: Iff.mpr, Set.image_nonempty, Function.monotone_eval, Monotone.map_bddAbove, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddBelow x
x_1 : ι
rw : IsGLB (eval (β := α) x_1 '' x) (sInf (eval (β := α) x_1 '' x))
⊢ IsGLB (eval (β := α) x_1 '' x) (sInf x x_1)

Tactic:
rw [sInf_apply_eq_sInf_image]

Premises used: sInf_apply_eq_sInf_image
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddBelow x
x_1 : ι
⊢ IsGLB (eval (β := α) x_1 '' x) (sInf (eval (β := α) x_1 '' x))

Tactic:
isGLB_csInf (image_nonempty.mpr hn) ((monotone_eval _).map_bddBelow hb)

Premises used: Iff.mpr, Set.image_nonempty, Function.monotone_eval, isGLB_csInf, Monotone.map_bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι_1 : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → ConditionallyCompleteLattice (α i)
x : Set ((i : ι) → α i)
hn : x.Nonempty
hb : BddBelow x
x_1 : ι
⊢ IsGLB (eval (β := α) x_1 '' x) (sInf (eval (β := α) x_1 '' x))

Tactic:
exact isGLB_csInf (image_nonempty.mpr hn) ((monotone_eval _).map_bddBelow hb)

Premises used: Iff.mpr, Set.image_nonempty, Function.monotone_eval, isGLB_csInf, Monotone.map_bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : b < sSup s
contrapose! : ∀ (hb : ∀ (a : α) (_ : a ∈ s), a ≤ b), sSup s ≤ b
⊢ ∃ a ∈ s, b < a

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

Tactic:
csSup_le hs hb

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

Tactic:
exact csSup_le hs hb

Premises used: csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
b : α
hs : s.Nonempty
hb : sInf s < b
⊢ ∃ a ∈ s, a < b

Tactic:
exists_lt_of_lt_csSup (α := αᵒᵈ) hs hb

Premises used: Set.Mem, exists_lt_of_lt_csSup, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
a : α
hb : BddAbove s
hs : s.Nonempty
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
lt_isLUB_iff <| isLUB_csSup hs hb

Premises used: lt_isLUB_iff, isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
a : α
hb : BddBelow s
hs : s.Nonempty
⊢ sInf s < a ↔ ∃ b ∈ s, b < a

Tactic:
isGLB_lt_iff <| isGLB_csInf hs hb

Premises used: isGLB_lt_iff, isGLB_csInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove s hs

Premises used: ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) (sSup ∅)

Tactic:
csSup_of_not_bddAbove hf

Premises used: iSup, csSup_of_not_bddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
rw : ¬BddAbove.{u_1} (α := α) univ
⊢ sSup s = sSup univ

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]

Premises used: csSup_of_not_bddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddAbove s
contrapose : ∀ (hs : BddAbove.{u_1} (α := α) univ), BddAbove s
⊢ ¬BddAbove.{u_1} (α := α) univ

Tactic:
contrapose hs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : BddAbove.{u_1} (α := α) univ
⊢ BddAbove s

Tactic:
hs.mono (subset_univ _)

Premises used: Set.subset_univ, BddAbove.mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : BddAbove.{u_1} (α := α) univ
⊢ BddAbove s

Tactic:
exact hs.mono (subset_univ _)

Premises used: Set.subset_univ, BddAbove.mono
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), f i) (sSup univ)

Tactic:
csSup_eq_univ_of_not_bddAbove hf

Premises used: iSup, csSup_eq_univ_of_not_bddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow s hs

Premises used: ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ι), f i) (sInf ∅)

Tactic:
csInf_of_not_bddBelow hf

Premises used: csInf_of_not_bddBelow, iInf
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : ¬BddBelow s
⊢ sInf s = sInf univ

Tactic:
csSup_eq_univ_of_not_bddAbove (α := αᵒᵈ) hs

Premises used: OrderDual, csSup_eq_univ_of_not_bddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
hf : ¬BddBelow (range f)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ι), f i) (sInf univ)

Tactic:
csInf_eq_univ_of_not_bddBelow hf

Premises used: iInf, csInf_eq_univ_of_not_bddBelow