awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
s : Set γ
a b : γ
ha : IsLUB s a
hb : b ∈ s
⊢ IsLUB (s ∩ Ici b) a

Tactic:
⟨fun _ hx => ha.1 hx.1, fun c hc =>
    have hbc : b ≤ c := hc ⟨hb, le_rfl⟩
    ha.2 fun x hx => ((le_total x b).elim fun hxb => hxb.trans hbc) fun hbx => hc ⟨hx, hbx⟩⟩

Premises used: le_rfl, le_total, IsLeast, And.right, And.left, And.intro, IsLUB, LE.le.trans, Or.elim
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
s : Set γ
x₀ : γ
rw : Monotone (β := Prop) fun (x : γ) ↦ ∀ y ∈ s, y ≤ x
⊢ BddAbove s ↔ ∃ (x : γ), x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Tactic:
rw [bddAbove_def, exists_ge_and_iff_exists]

Premises used: exists_ge_and_iff_exists, bddAbove_def
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone (β := Prop) fun (x : γ) ↦ ∀ y ∈ s, y ≤ x

Tactic:
Monotone.ball fun x _ => monotone_le

Premises used: Monotone.ball, monotone_le
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ Monotone (β := Prop) fun (x : γ) ↦ ∀ y ∈ s, y ≤ x

Tactic:
exact Monotone.ball fun x _ => monotone_le

Premises used: Monotone.ball, monotone_le
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeInf γ
s : Set γ
x₀ : γ
⊢ BddBelow s ↔ ∃ x ≤ x₀, ∀ y ∈ s, x ≤ y

Tactic:
bddAbove_iff_exists_ge (toDual x₀)

Premises used: OrderDual.toDual, bddAbove_iff_exists_ge, lowerBounds, Set.Mem, setOf, BddBelow, OrderDual, DFunLike.coe
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
s : Set γ
hs : BddAbove s
x₀ : γ
⊢ ∃ (x : γ), x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x

Tactic:
(bddAbove_iff_exists_ge x₀).mp hs

Premises used: bddAbove_iff_exists_ge, Iff.mp
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsLeast (Ici a) a

Tactic:
⟨self_mem_Ici, fun _ => id⟩

Premises used: id, IsLeast, And.intro, Set.self_mem_Ici
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsLUB (Iic a) a

Tactic:
isGreatest_Iic.isLUB

Premises used: IsGreatest.isLUB, isGreatest_Iic
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ upperBounds (Iic a) = Ici a

Tactic:
isLUB_Iic.upperBounds_eq

Premises used: IsLUB.upperBounds_eq, isLUB_Iic
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ BddAbove (Iic a)

Tactic:
isLUB_Iic.bddAbove

Premises used: IsLUB.bddAbove, isLUB_Iic
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ BddAbove (Iio a)

Tactic:
⟨a, fun _ hx => le_of_lt hx⟩

Premises used: le_of_lt, BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
b a : α
hb : IsLUB (Iio a) b
⊢ b ≤ a

Tactic:
(isLUB_le_iff hb).mpr fun _ hk => le_of_lt hk

Premises used: Iff.mpr, le_of_lt, isLUB_le_iff
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
inl : ∀ (hj_eq_i : j = i), j = i ∨ Iio i = Iic j
inr : ∀ (hj_lt_i : j < i), j = i ∨ Iio i = Iic j
⊢ j = i ∨ Iio i = Iic j

Tactic:
rcases eq_or_lt_of_le (le_of_isLUB_Iio i hj) with hj_eq_i | hj_lt_i

Premises used: le_of_isLUB_Iio, eq_or_lt_of_le
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

Tactic:
Or.inl hj_eq_i

Premises used: Or.inl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_eq_i : j = i
⊢ j = i ∨ Iio i = Iic j

Tactic:
exact Or.inl hj_eq_i

Premises used: Or.inl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
inr : Iio i = Iic j
⊢ j = i ∨ Iio i = Iic j

Tactic:
right
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j

Tactic:
Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

Premises used: Set.ext, lt_of_le_of_lt, And.left, Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j

Tactic:
exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

Premises used: Set.ext, lt_of_le_of_lt, And.left, Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
pos : ∀ (h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i), ∃ (j : γ), IsLUB (Iio i) j
neg : ∀ (h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j), ∃ (j : γ), IsLUB (Iio i) j
⊢ ∃ (j : γ), IsLUB (Iio i) j

Tactic:
by_cases! h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i

Premises used: upperBounds, Set.Iio
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i
pos : ∀ (j : γ) (hj_ub : j ∈ upperBounds (Iio i)) (hj_lt_i : j < i), ∃ (j : γ), IsLUB (Iio i) j
⊢ ∃ (j : γ), IsLUB (Iio i) j

Tactic:
obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ (j : γ), IsLUB (Iio i) j

Tactic:
⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i j : γ
hj_ub : j ∈ upperBounds (Iio i)
hj_lt_i : j < i
⊢ ∃ (j : γ), IsLUB (Iio i) j

Tactic:
exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j
⊢ ∃ (j : γ), IsLUB (Iio i) j

Tactic:
⟨i, fun j hj => le_of_lt hj, ?_⟩

Premises used: le_of_lt, And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j
neg : i ∈ lowerBounds (upperBounds (Iio i))
⊢ ∃ (j : γ), IsLUB (Iio i) j

Tactic:
refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j
⊢ ∀ x ∈ upperBounds (Iio i), i ≤ x

Tactic:
h_exists_lt
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j
⊢ ∀ x ∈ upperBounds (Iio i), i ≤ x

Tactic:
exact h_exists_lt
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
inst_1 : DenselyOrdered γ
a : γ
⊢ IsLUB (Iio a) a

Tactic:
⟨fun _ hx => le_of_lt hx, fun _ hy => le_of_forall_lt_imp_le_of_dense hy⟩

Premises used: le_of_forall_lt_imp_le_of_dense, le_of_lt, IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
inst_1 : DenselyOrdered γ
a : γ
⊢ upperBounds (Iio a) = Ici a

Tactic:
isLUB_Iio.upperBounds_eq

Premises used: isLUB_Iio, IsLUB.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsGreatest {a} a

Tactic:
⟨mem_singleton a, fun _ hx => le_of_eq <| eq_of_mem_singleton hx⟩

Premises used: Set.mem_singleton, Set.eq_of_mem_singleton, IsGreatest, And.intro, le_of_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsLUB {a} a

Tactic:
isGreatest_singleton.isLUB

Premises used: IsGreatest.isLUB, isGreatest_singleton
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ BddAbove (α := α) {a}

Tactic:
isLUB_singleton.bddAbove

Premises used: isLUB_singleton, IsLUB.bddAbove
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ upperBounds {a} = Ici a

Tactic:
isLUB_singleton.upperBounds_eq

Premises used: isLUB_singleton, IsLUB.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddAbove (Icc a b)

Tactic:
⟨b, fun _ => And.right⟩

Premises used: BddAbove, Set.Nonempty, And.right, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddBelow (Icc a b)

Tactic:
⟨a, fun _ => And.left⟩

Premises used: Set.Nonempty, And.left, BddBelow, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddAbove (Ico a b)

Tactic:
bddAbove_Icc.mono Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, bddAbove_Icc, BddAbove.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddBelow (Ico a b)

Tactic:
bddBelow_Icc.mono Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, BddBelow.mono, bddBelow_Icc
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddAbove (Ioc a b)

Tactic:
bddAbove_Icc.mono Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, bddAbove_Icc, BddAbove.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddBelow (Ioc a b)

Tactic:
bddBelow_Icc.mono Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, BddBelow.mono, bddBelow_Icc
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddAbove (Ioo a b)

Tactic:
bddAbove_Icc.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, bddAbove_Icc, BddAbove.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ BddBelow (Ioo a b)

Tactic:
bddBelow_Icc.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, BddBelow.mono, bddBelow_Icc
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ IsGreatest (Icc a b) b

Tactic:
⟨right_mem_Icc.2 h, fun _ => And.right⟩

Premises used: Iff.mpr, Set.right_mem_Icc, IsGreatest, And.right, And.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ IsLUB (Icc a b) b

Tactic:
(isGreatest_Icc h).isLUB

Premises used: IsGreatest.isLUB, isGreatest_Icc
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ upperBounds (Icc a b) = Ici b

Tactic:
(isLUB_Icc h).upperBounds_eq

Premises used: IsLUB.upperBounds_eq, isLUB_Icc
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ IsLeast (Icc a b) a

Tactic:
⟨left_mem_Icc.2 h, fun _ => And.left⟩

Premises used: Iff.mpr, IsLeast, And.left, Set.left_mem_Icc, And.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ IsGLB (Icc a b) a

Tactic:
(isLeast_Icc h).isGLB

Premises used: isLeast_Icc, IsLeast.isGLB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a ≤ b
⊢ lowerBounds (Icc a b) = Iic a

Tactic:
(isGLB_Icc h).lowerBounds_eq

Premises used: isGLB_Icc, IsGLB.lowerBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ IsGreatest (Ioc a b) b

Tactic:
⟨right_mem_Ioc.2 h, fun _ => And.right⟩

Premises used: Iff.mpr, IsGreatest, And.right, And.intro, Set.right_mem_Ioc
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ IsLUB (Ioc a b) b

Tactic:
(isGreatest_Ioc h).isLUB

Premises used: isGreatest_Ioc, IsGreatest.isLUB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ upperBounds (Ioc a b) = Ici b

Tactic:
(isLUB_Ioc h).upperBounds_eq

Premises used: isLUB_Ioc, IsLUB.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ IsLeast (Ico a b) a

Tactic:
⟨left_mem_Ico.2 h, fun _ => And.left⟩

Premises used: Iff.mpr, Set.left_mem_Ico, IsLeast, And.left, And.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ IsGLB (Ico a b) a

Tactic:
(isLeast_Ico h).isGLB

Premises used: IsLeast.isGLB, isLeast_Ico
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : a < b
⊢ lowerBounds (Ico a b) = Iic a

Tactic:
(isGLB_Ico h).lowerBounds_eq

Premises used: isGLB_Ico, IsGLB.lowerBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
inl : ∀ (h₁ : a = x ⊔ a), x ≤ a
inr : ∀ (h₂ : a < x ⊔ a), x ≤ a
⊢ x ≤ a

Tactic:
rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂

Premises used: le_sup_right, eq_or_lt_of_le
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₁ : a = x ⊔ a
⊢ x ≤ a

Tactic:
h₁.symm ▸ le_sup_left

Premises used: le_sup_left, Eq.rec, Eq.symm
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₁ : a = x ⊔ a
⊢ x ≤ a

Tactic:
exact h₁.symm ▸ le_sup_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
inr : ∀ (y : γ) (lty : a < y) (ylt : y < x ⊔ a), x ≤ a
⊢ x ≤ a

Tactic:
obtain ⟨y, lty, ylt⟩ := exists_between h₂

Premises used: exists_between
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
apply : x ≤ b
⊢ x ≤ a

Tactic:
apply (not_lt_of_ge (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim

Premises used: False.elim, LT.lt.le, LT.lt.trans_le, And.intro, sup_le, not_lt_of_ge
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
obtain : ∀ (u : γ) (au : a < u) (ub : u < b), x ≤ b
⊢ x ≤ b

Tactic:
obtain ⟨u, au, ub⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
u : γ
au : a < u
ub : u < b
⊢ x ≤ b

Tactic:
apply (hx ⟨au, ub⟩).trans ub.le

Premises used: LT.lt.le, And.intro, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ lowerBounds (Ioo a b) = Iic a

Tactic:
(isGLB_Ioo hab).lowerBounds_eq

Premises used: isGLB_Ioo, IsGLB.lowerBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsGLB (Ioc a b) a

Tactic:
(isGLB_Ioo hab).of_subset_of_superset (isGLB_Icc hab.le) Ioo_subset_Ioc_self Ioc_subset_Icc_self

Premises used: IsGLB.of_subset_of_superset, Set.Ioc_subset_Icc_self, isGLB_Ioo, LT.lt.le, isGLB_Icc, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ lowerBounds (Ioc a b) = Iic a

Tactic:
(isGLB_Ioc hab).lowerBounds_eq

Premises used: isGLB_Ioc, IsGLB.lowerBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeInf γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ioo a b) b

Tactic:
simpa only [Ioo_toDual] using isGLB_Ioo hab.dual

Premises used: isGLB_Ioo, Set.Ioo_toDual, LT.lt.dual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeInf γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ upperBounds (Ioo a b) = Ici b

Tactic:
(isLUB_Ioo hab).upperBounds_eq

Premises used: isLUB_Ioo, IsLUB.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeInf γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ico a b) b

Tactic:
simpa only [Ioc_toDual] using isGLB_Ioc hab.dual

Premises used: Set.Ioc_toDual, isGLB_Ioc, LT.lt.dual
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeInf γ
inst_1 : DenselyOrdered γ
a b : γ
hab : a < b
⊢ upperBounds (Ico a b) = Ici b

Tactic:
(isLUB_Ico hab).upperBounds_eq

Premises used: isLUB_Ico, IsLUB.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ BddBelow s ↔ ∃ (a : α), s ⊆ Ici a

Tactic:
Iff.rfl

Premises used: Set.Ici, lowerBounds, Set.Mem, Iff.rfl, setOf, Set.Subset, Set.Nonempty, BddBelow
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ BddBelow s ∧ BddAbove s ↔ ∃ (a : α) (b : α), s ⊆ Icc a b

Tactic:
simp [Ici_inter_Iic.symm, subset_inter_iff, bddBelow_iff_subset_Ici,
    bddAbove_iff_subset_Iic, exists_and_left, exists_and_right]

Premises used: Set.subset_inter_iff, bddAbove_iff_subset_Iic, exists_and_left, exists_and_right, bddBelow_iff_subset_Ici, Eq.symm, Set.Ici_inter_Iic
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsGreatest univ a ↔ IsTop a

Tactic:
simp [IsGreatest, mem_upperBounds, IsTop]

Premises used: IsGreatest, IsTop, mem_upperBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ IsGreatest.{u_1} (α := α) univ ⊤

Tactic:
isGreatest_univ_iff.2 isTop_top

Premises used: Iff.mpr, isGreatest_univ_iff, isTop_top
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderTop γ
rw : Eq (α := Set γ) (Ici ⊤) {⊤}
rw₁ rw₂ : Eq (α := Set γ) {⊤} {⊤}
⊢ Eq (α := Set γ) (upperBounds univ) {⊤}

Tactic:
rw [isGreatest_univ.upperBounds_eq, Ici_top]

Premises used: isGreatest_univ, Set.Ici_top, IsGreatest.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ IsLUB.{u_1} (α := α) univ ⊤

Tactic:
isGreatest_univ.isLUB

Premises used: isGreatest_univ, IsGreatest.isLUB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoTopOrder α
⊢ Eq.{u_1 + 1} (α := Set α) (upperBounds univ) ∅

Tactic:
eq_empty_of_subset_empty fun b hb =>
    not_isTop b fun x => hb (mem_univ x)

Premises used: Set.eq_empty_of_subset_empty, not_isTop, Set.mem_univ
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoTopOrder α
⊢ ¬BddAbove.{u_1} (α := α) univ

Tactic:
simp [BddAbove]

Premises used: BddAbove
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := Set α) (upperBounds ∅) univ

Tactic:
simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, forall_mem_empty, forall_true_iff]

Premises used: Set.eq_univ_iff_forall, upperBounds, Set.mem_setOf_eq, forall_true_iff, Set.forall_mem_empty
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ BddAbove.{u_1} (α := α) ∅

Tactic:
simp only [BddAbove, upperBounds_empty, univ_nonempty]

Premises used: upperBounds_empty, Set.univ_nonempty, BddAbove
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsGLB ∅ a ↔ IsTop a

Tactic:
simp [IsGLB]

Premises used: IsGLB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
⊢ IsGLB.{u_1} (α := α) ∅ ⊤

Tactic:
isGLB_empty_iff.2 isTop_top

Premises used: Iff.mpr, isGLB_empty_iff, isTop_top
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
inst_1 : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x : α
rw : Membership.mem (γ := Set α) univ x
⊢ x ∈ upperBounds s

Tactic:
rw [h, upperBounds_empty]

Premises used: upperBounds_empty
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
inst_1 : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
inst_1 : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
ha : Nonempty α
h : ¬BddAbove s
⊢ s.Nonempty

Tactic:
(Nonempty.elim ha) fun x => (not_bddAbove_iff'.1 h x).imp fun _ ha => ha.1

Premises used: Nonempty.elim, Exists.imp, Iff.mp, not_bddAbove_iff'
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s : Set α
a : α
⊢ BddAbove (insert a s) ↔ BddAbove s

Tactic:
simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and]

Premises used: Set.insert_eq, bddAbove_union, bddAbove_singleton, true_and
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s : Set α
a : α
⊢ BddAbove s → BddAbove (insert a s)

Tactic:
bddAbove_insert.2

Premises used: Iff.mpr, bddAbove_insert
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)

Tactic:
isLUB_singleton.union hs

Premises used: IsLUB.union, isLUB_singleton
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
a b : γ
s : Set γ
hs : IsLUB s b
⊢ IsLUB ({a} ∪ s) (a ⊔ b)

Tactic:
exact isLUB_singleton.union hs

Premises used: IsLUB.union, isLUB_singleton
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)

Tactic:
isGreatest_singleton.union hs

Premises used: isGreatest_singleton, IsGreatest.union
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
s : Set γ
hs : IsGreatest s b
⊢ IsGreatest ({a} ∪ s) (max a b)

Tactic:
exact isGreatest_singleton.union hs

Premises used: isGreatest_singleton, IsGreatest.union
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
s : Set α
rw : upperBounds ({a} ∪ s) = Ici a ∩ upperBounds s
rw₁ : upperBounds {a} ∩ upperBounds s = Ici a ∩ upperBounds s
rw₂ rw₃ : Ici a ∩ upperBounds s = Ici a ∩ upperBounds s
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s

Tactic:
rw [insert_eq, upperBounds_union, upperBounds_singleton]

Premises used: Set.insert_eq, upperBounds_union, upperBounds_singleton
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
s : Set α
⊢ BddAbove s

Tactic:
⟨⊤, fun a _ => OrderTop.le_top a⟩

Premises used: OrderTop.le_top, BddAbove, Set.Nonempty, Exists.intro, Top.top
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
a b : γ
⊢ IsLUB {a, b} (a ⊔ b)

Tactic:
isLUB_singleton.insert _

Premises used: isLUB_singleton, IsLUB.insert
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
⊢ IsGreatest {a, b} (max a b)

Tactic:
isGreatest_singleton.insert _

Premises used: IsGreatest.insert, isGreatest_singleton
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
⊢ IsLUB (lowerBounds s) a ↔ IsGLB s a

Tactic:
⟨fun H => ⟨fun _ hx => H.2 <| subset_upperBounds_lowerBounds s hx, H.1⟩, IsGreatest.isLUB⟩

Premises used: IsGreatest.isLUB, And.right, And.left, And.intro, subset_upperBounds_lowerBounds, Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x y : α) ↦ y ≤ x) s
hMin : Minimal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
obtain : ∀ (z : α) (hz : z ∈ s) (hza : z ≤ a) (hzb : z ≤ b), a ≤ b
⊢ a ≤ b

Tactic:
obtain ⟨z, hz, hza, hzb⟩ := h a hMin.1 b hb

Premises used: And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x y : α) ↦ y ≤ x) s
hMin : Minimal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
z : α
hz : z ∈ s
hza : z ≤ a
hzb : z ≤ b
⊢ a ≤ b

Tactic:
(hMin.2 hz hza).trans hzb

Premises used: And.right, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x y : α) ↦ y ≤ x) s
hMin : Minimal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
z : α
hz : z ∈ s
hza : z ≤ a
hzb : z ≤ b
⊢ a ≤ b

Tactic:
exact (hMin.2 hz hza).trans hzb

Premises used: And.right, LE.le.trans