awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
inl :
  ∀ (hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y)
    (ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x), sSup ∅ = sSup t
inr : ∀ (s_ne : s.Nonempty), sSup s = sSup t
⊢ sSup s = sSup t

Tactic:
rcases eq_empty_or_nonempty s with rfl | s_ne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x
y : α
yt : y ∈ t
⊢ False

Tactic:
simpa using ht y yt
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x
⊢ t = ∅

Tactic:
have : t = ∅ := eq_empty_of_forall_notMem (fun y yt ↦ by simpa using ht y yt)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
t : Set α
hs : ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ y ≤ x
this : t = ∅
inl inl₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ sSup ∅ = sSup t

Tactic:
rw [this]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
inr :
  ∀ (hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y)
    (ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x), sSup s = sSup ∅
inr₁ : ∀ (t_ne : t.Nonempty), sSup s = sSup t
⊢ sSup s = sSup t

Tactic:
rcases eq_empty_or_nonempty t with rfl | t_ne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y
ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x
x : α
xs : x ∈ s
⊢ False

Tactic:
simpa using hs x xs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y
ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x
⊢ s = ∅

Tactic:
have : s = ∅ := eq_empty_of_forall_notMem (fun x xs ↦ by simpa using hs x xs)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
s_ne : s.Nonempty
hs : ∀ x ∈ s, ∃ (y : α), Membership.mem (γ := Set α) ∅ y ∧ x ≤ y
ht : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ x ∈ s, y ≤ x
this : s = ∅
inr inr₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
⊢ sSup s = sSup ∅

Tactic:
rw [this]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
pos : ∀ (B : BddAbove s ∨ BddAbove t), sSup s = sSup t
neg : ∀ (B : ¬(BddAbove s ∨ BddAbove t)), sSup s = sSup t
⊢ sSup s = sSup t

Tactic:
by_cases B : BddAbove s ∨ BddAbove t

Premises used: BddAbove
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
inl : ∀ (hB : BddAbove s), BddAbove s
inr : ∀ (b : α) (hb : b ∈ upperBounds t), BddAbove s
⊢ BddAbove s

Tactic:
rcases B with hB | ⟨b, hb⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
hB : BddAbove s
⊢ BddAbove s

Tactic:
hB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
hB : BddAbove s
⊢ BddAbove s

Tactic:
exact hB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
⊢ BddAbove s

Tactic:
⟨b, fun x hx ↦ ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
inr : ∀ (x : α) (hx : x ∈ s), x ≤ b
⊢ BddAbove s

Tactic:
refine ⟨b, fun x hx ↦ ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
inr : ∀ (y : α) (hy : y ∈ t) (hxy : x ≤ y), x ≤ b
⊢ x ≤ b

Tactic:
rcases hs x hx with ⟨y, hy, hxy⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : x ≤ y
⊢ x ≤ b

Tactic:
hxy.trans (hb hy)

Premises used: LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
b : α
hb : b ∈ upperBounds t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : x ≤ y
⊢ x ≤ b

Tactic:
exact hxy.trans (hb hy)

Premises used: LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
⊢ BddAbove s

Tactic:
have Bs : BddAbove s := by
      rcases B with hB | ⟨b, hb⟩
      · exact hB
      · refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
inl : ∀ (b : α) (hb : b ∈ upperBounds s), BddAbove t
inr : ∀ (hB : BddAbove t), BddAbove t
⊢ BddAbove t

Tactic:
rcases B with ⟨b, hb⟩ | hB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
⊢ BddAbove t

Tactic:
⟨b, fun y hy ↦ ?_⟩

Premises used: BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
inl : ∀ (y : α) (hy : y ∈ t), y ≤ b
⊢ BddAbove t

Tactic:
refine ⟨b, fun y hy ↦ ?_⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
y : α
hy : y ∈ t
inl : ∀ (x : α) (hx : x ∈ s) (hyx : y ≤ x), y ≤ b
⊢ y ≤ b

Tactic:
rcases ht y hy with ⟨x, hx, hyx⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
y : α
hy : y ∈ t
x : α
hx : x ∈ s
hyx : y ≤ x
⊢ y ≤ b

Tactic:
hyx.trans (hb hx)

Premises used: LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
b : α
hb : b ∈ upperBounds s
y : α
hy : y ∈ t
x : α
hx : x ∈ s
hyx : y ≤ x
⊢ y ≤ b

Tactic:
exact hyx.trans (hb hx)

Premises used: LE.le.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
hB : BddAbove t
⊢ BddAbove t

Tactic:
hB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
hB : BddAbove t
⊢ BddAbove t

Tactic:
exact hB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
⊢ BddAbove t

Tactic:
have Bt : BddAbove t := by
      rcases B with ⟨b, hb⟩ | hB
      · refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)
      · exact hB
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
pos : sSup s ≤ sSup t
pos₁ : sSup t ≤ sSup s
⊢ sSup s = sSup t

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
apply : ∀ (x : α) (hx : x ∈ s), x ≤ sSup t
⊢ sSup s ≤ sSup t

Tactic:
apply csSup_le s_ne (fun x hx ↦ ?_)

Premises used: csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
rcases : ∀ (y : α) (yt : y ∈ t) (hxy : x ≤ y), x ≤ sSup t
⊢ x ≤ sSup t

Tactic:
rcases hs x hx with ⟨y, yt, hxy⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
y : α
yt : y ∈ t
hxy : x ≤ y
⊢ x ≤ sSup t

Tactic:
hxy.trans (le_csSup Bt yt)

Premises used: LE.le.trans, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
x : α
hx : x ∈ s
y : α
yt : y ∈ t
hxy : x ≤ y
⊢ x ≤ sSup t

Tactic:
exact hxy.trans (le_csSup Bt yt)

Premises used: LE.le.trans, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
apply : ∀ (y : α) (hy : y ∈ t), y ≤ sSup s
⊢ sSup t ≤ sSup s

Tactic:
apply csSup_le t_ne (fun y hy ↦ ?_)

Premises used: csSup_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
y : α
hy : y ∈ t
rcases : ∀ (x : α) (xs : x ∈ s) (hyx : y ≤ x), y ≤ sSup s
⊢ y ≤ sSup s

Tactic:
rcases ht y hy with ⟨x, xs, hyx⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
y : α
hy : y ∈ t
x : α
xs : x ∈ s
hyx : y ≤ x
⊢ y ≤ sSup s

Tactic:
hyx.trans (le_csSup Bs xs)

Premises used: LE.le.trans, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
y : α
hy : y ∈ t
x : α
xs : x ∈ s
hyx : y ≤ x
⊢ y ≤ sSup s

Tactic:
exact hyx.trans (le_csSup Bs xs)

Premises used: LE.le.trans, le_csSup
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : ¬(BddAbove s ∨ BddAbove t)
⊢ sSup s = sSup t

Tactic:
simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]

Premises used: csSup_of_not_bddAbove, not_or, And.right, And.left, Iff.mp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x
ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
⊢ sInf s = sInf t

Tactic:
csSup_eq_csSup_of_forall_exists_le (α := αᵒᵈ) hs ht

Premises used: OrderDual, csSup_eq_csSup_of_forall_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
inl : sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)
inr : ∀ (hs : 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 | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
t : Set α
⊢ sSup (∅ ∪ t) ≤ max (sSup ∅) (sSup t)

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
inr : sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)
inr₁ : ∀ (ht : t.Nonempty), sSup (s ∪ t) ≤ max (sSup s) (sSup t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.Nonempty
⊢ sSup (s ∪ ∅) ≤ max (sSup s) (sSup ∅)

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
pos : BddAbove (s ∪ t) → sSup (s ∪ t) ≤ max (sSup s) (sSup t)
neg : ¬BddAbove (s ∪ t) → sSup (s ∪ t) ≤ max (sSup s) (sSup t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
by_cases BddAbove (s ∪ t)

Premises used: BddAbove, Union.union
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h : BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
grind [csSup_union, bddAbove_union, csSup_of_not_bddAbove]

Premises used: bddAbove_union, csSup_of_not_bddAbove, csSup_union
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
h : ¬BddAbove (s ∪ t)
⊢ sSup (s ∪ t) ≤ max (sSup s) (sSup t)

Tactic:
grind [csSup_union, bddAbove_union, csSup_of_not_bddAbove]

Premises used: bddAbove_union, csSup_of_not_bddAbove, csSup_union
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
hs :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x →
      ∃ (y : α), Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y ∧ x ≤ y
ht :
  ∀ (y : α),
    Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y →
      ∃ (x : α), Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x ∧ y ≤ x
⊢ Eq.{u_1 + 1} (α := α) (sSup (⋃ (i : ι), Iic (f i))) (⨆ (i : ι), f i)

Tactic:
apply csSup_eq_csSup_of_forall_exists_le

Premises used: csSup_eq_csSup_of_forall_exists_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
x : α
i : ι
hi : Membership.mem (γ := Set α) ((fun (i : ι) ↦ Iic (f i)) i) x
⊢ ∃ (y : α), Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y ∧ x ≤ y

Tactic:
⟨f i, mem_range_self _, hi⟩

Premises used: Set.mem_range_self, And.intro, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
x : α
i : ι
hi : Membership.mem (γ := Set α) ((fun (i : ι) ↦ Iic (f i)) i) x
⊢ ∃ (y : α), Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) y ∧ x ≤ y

Tactic:
exact ⟨f i, mem_range_self _, hi⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
i : ι
⊢ ∃ (x : α), Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x ∧ (fun (i : ι) ↦ f i) i ≤ x

Tactic:
⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

Premises used: le_rfl, And.intro, Set.mem_iUnion_of_mem, Exists.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
i : ι
⊢ ∃ (x : α), Membership.mem (γ := Set α) (⋃ (i : ι), Iic (f i)) x ∧ (fun (i : ι) ↦ f i) i ≤ x

Tactic:
exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (sInf (⋃ (i : ι), Ici (f i))) (⨅ (i : ι), f i)

Tactic:
sSup_iUnion_Iic (α := αᵒᵈ) f

Premises used: iInf, Set.Ici, setOf, OrderDual, sSup_iUnion_Iic
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : OrderBot α
s : Set α
hs : ⊥ ∈ s
⊢ sInf s = ⊥

Tactic:
eq_bot_iff.2 <| csInf_le (OrderBot.bddBelow s) hs

Premises used: Iff.mpr, OrderBot.bddBelow, eq_bot_iff, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : OrderTop α
s : Set α
hs : ⊤ ∈ s
⊢ sSup s = ⊤

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

Premises used: csInf_eq_bot_of_bot_mem, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
⊢ sInf s = argminOn id s hs

Tactic:
IsLeast.csInf_eq ⟨argminOn_mem _ _ _, fun _ ha => argminOn_le id _ ha⟩

Premises used: IsLeast.csInf_eq, id, Function.argminOn_mem, Function.argminOn_le, And.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
rw : IsLeast s (argminOn id s hs)
⊢ IsLeast s (sInf s)

Tactic:
rw [sInf_eq_argmin_on hs]

Premises used: sInf_eq_argmin_on
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)

Tactic:
⟨argminOn_mem _ _ _, fun a ha => argminOn_le id _ ha⟩

Premises used: id, Function.argminOn_mem, Function.argminOn_le, IsLeast, And.intro
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)

Tactic:
exact ⟨argminOn_mem _ _ _, fun a ha => argminOn_le id _ ha⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
b : α
inst_1 : WellFoundedLT α
hs : s.Nonempty
⊢ b ≤ sInf s ↔ b ∈ lowerBounds s

Tactic:
le_isGLB_iff (isLeast_csInf hs).isGLB

Premises used: isLeast_csInf, IsLeast.isGLB, le_isGLB_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
⊢ sInf s ∈ s

Tactic:
(isLeast_csInf hs).1

Premises used: isLeast_csInf, And.left
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
have : ∀ (this : OrderBot α), sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a

Tactic:
have : OrderBot α := WellFoundedLT.toOrderBot α
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
mp : sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a
mpr : (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a

Tactic:
constructor
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
this : OrderBot α
⊢ sInf s ∈ s ∧ ∀ a ∈ s, sInf s ≤ a

Tactic:
⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩

Premises used: csInf_mem, And.intro, OrderBot.bddBelow, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
this : OrderBot α
⊢ sInf s ∈ s ∧ ∀ a ∈ s, sInf s ≤ a

Tactic:
exact ⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
hn : n ∈ s
hle : ∀ a ∈ s, n ≤ a
⊢ sInf s = n

Tactic:
le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)

Premises used: le_csInf, le_antisymm, OrderBot.bddBelow, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
hn : n ∈ s
hle : ∀ a ∈ s, n ≤ a
⊢ sInf s = n

Tactic:
exact le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)

Premises used: le_csInf, le_antisymm, OrderBot.bddBelow, csInf_le
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
s : Set α
inst_1 : WellFoundedLT α
β : Type u_5
inst_2 : ConditionallyCompleteLattice β
f : α → β
hf : MonotoneOn f s
hs : s.Nonempty
⊢ f (sInf s) = sInf (f '' s)

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

Premises used: isLeast_csInf, IsLeast.csInf_eq, MonotoneOn.map_isLeast, Eq.symm