awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
refine_2 :
  ∀ (y' : α) (hy' : y' ∈ s) (hyy' : y ≤ y'),
    ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨y', hy', hyy'⟩ := hts.union_right hy

Premises used: IsCofinalFor.union_right
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
y' : α
hy' : y' ∈ s
hyy' : y ≤ y'
refine_2 :
  ∀ (z : α) (hz : z ∈ s) (hx'z : x' ≤ z) (hy'z : y' ≤ z),
    ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨z, hz, hx'z, hy'z⟩ := hs x' hx' y' hy'
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
y' : α
hy' : y' ∈ s
hyy' : y ≤ y'
z : α
hz : z ∈ s
hx'z : x' ≤ z
hy'z : y' ≤ z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

Premises used: And.intro, Exists.intro, Or.inl, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ s
hxx' : x ≤ x'
y' : α
hy' : y' ∈ s
hyy' : y ≤ y'
z : α
hz : z ∈ s
hx'z : x' ≤ z
hy'z : y' ≤ z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
exact ⟨z, .inl hz, hxx'.trans hx'z, hyy'.trans hy'z⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
refine_2 :
  ∀ (x' : α) (hx' : x' ∈ t) (hxx' : x ≤ x'),
    ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨x', hx', hxx'⟩ := hst.union_left hx

Premises used: IsCofinalFor.union_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
refine_2 :
  ∀ (y' : α) (hy' : y' ∈ t) (hyy' : y ≤ y'),
    ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨y', hy', hyy'⟩ := hst.union_left hy

Premises used: IsCofinalFor.union_left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
y' : α
hy' : y' ∈ t
hyy' : y ≤ y'
refine_2 :
  ∀ (z : α) (hz : z ∈ t) (hx'z : x' ≤ z) (hy'z : y' ≤ z),
    ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
y' : α
hy' : y' ∈ t
hyy' : y ≤ y'
z : α
hz : z ∈ t
hx'z : x' ≤ z
hy'z : y' ≤ z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
⟨z, .inr hz, hxx'.trans hx'z, hyy'.trans hy'z⟩

Premises used: And.intro, Exists.intro, LE.le.trans, Or.inr
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
y' : α
hy' : y' ∈ t
hyy' : y ≤ y'
z : α
hz : z ∈ t
hx'z : x' ≤ z
hy'z : y' ≤ z
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
exact ⟨z, .inr hz, hxx'.trans hx'z, hyy'.trans hy'z⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
rw [directedOn_union_iff] at h

Premises used: directedOn_union_iff
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
inl :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s →
    IsCofinalFor t s → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inr :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t →
    IsCofinalFor s t → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inl₁ :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s →
    IsCofinalFor t s → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inr₁ :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t →
    IsCofinalFor s t → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inl₂ :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s →
    IsCofinalFor t s → ¬DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inr₂ :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t →
    IsCofinalFor s t → ¬DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inl₃ :
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s →
    IsCofinalFor t s →
      ¬DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s →
        ∀ x ∈ t, ∀ y ∈ t, ∃ z ∈ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t

Tactic:
tauto
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
inl :
  ∀ (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
inr :
  ∀ (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
obtain h | h := directedOn_or_directedOn_of_union h

Premises used: directedOn_or_directedOn_of_union
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
inl :
  ∀ (hn : (∅ ∪ t).Nonempty) (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (∅ ∪ t))
    (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅ ∧ Set.Nonempty.{u_1} (α := α) ∅ ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
inl₁ :
  ∀ (hs : s.Nonempty),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
t : Set α
hn : (∅ ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (∅ ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅ ∧ Set.Nonempty.{u_1} (α := α) ∅ ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
aesop
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
.inl ⟨h, hs⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
exact .inl ⟨h, hs⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
inr :
  ∀ (hn : (s ∪ ∅).Nonempty) (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ ∅))
    (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅ ∧ Set.Nonempty.{u_1} (α := α) ∅
inr₁ :
  ∀ (ht : t.Nonempty),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hn : (s ∪ ∅).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ ∅)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) ∅ ∧ Set.Nonempty.{u_1} (α := α) ∅

Tactic:
aesop
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
ht : t.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
.inr ⟨h, ht⟩

Premises used: And.intro, Or.inr
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
ht : t.Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty

Tactic:
exact .inr ⟨h, ht⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hst : s ⊆ t
⊢ upperBounds t ⊆ upperBounds s

Tactic:
fun _ hb _ h => hb <| hst h

Premises used: Set.Mem, setOf, upperBounds, Set.Subset
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hst : IsCofinalFor s t
⊢ upperBounds t ⊆ upperBounds s

Tactic:
fun _a ha _b hb ↦ let ⟨_c, hc, hbc⟩ := hst hb; hbc.trans (ha hc)

Premises used: Set.Mem, setOf, upperBounds, LE.le, Set.Subset, _private.0.IsCofinalFor.trans.match_1, LE.le.trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
hab : a ≤ b
⊢ a ∈ upperBounds s → b ∈ upperBounds s

Tactic:
fun ha _ h => le_trans (ha h) hab

Premises used: Set.Mem, setOf, upperBounds, le_trans
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hst : s ⊆ t
a b : α
hab : a ≤ b
⊢ a ∈ upperBounds t → b ∈ upperBounds s

Tactic:
fun ha =>
  upperBounds_mono_set hst <| upperBounds_mono_mem hab ha

Premises used: upperBounds_mono_set, upperBounds_mono_mem
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : s ⊆ t
⊢ BddAbove t → BddAbove s

Tactic:
Nonempty.mono <| upperBounds_mono_set h

Premises used: upperBounds_mono_set, BddAbove, Set.Nonempty.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
s t p : Set α
hs : IsLUB s a
hp : IsLUB p a
hst : s ⊆ t
htp : t ⊆ p
⊢ IsLUB t a

Tactic:
⟨upperBounds_mono_set htp hp.1, lowerBounds_mono_set (upperBounds_mono_set hst) hs.2⟩

Premises used: upperBounds_mono_set, lowerBounds_mono_set, IsLeast, And.right, And.left, And.intro, IsLUB
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
a b : α
ha : IsLeast s a
hb : IsLeast t b
hst : s ⊆ t
⊢ b ≤ a

Tactic:
hb.2 (hst ha.1)

Premises used: And.right, And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
a b : α
ha : IsLUB s a
hb : IsLUB t b
hst : s ⊆ t
⊢ a ≤ b

Tactic:
IsLeast.mono hb ha <| upperBounds_mono_set hst

Premises used: upperBounds_mono_set, IsLeast.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s ⊆ lowerBounds (upperBounds s)

Tactic:
fun _ hx _ hy => hy hx

Premises used: lowerBounds, Set.Mem, setOf, Set.Subset
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : s.Nonempty
⊢ BddAbove (lowerBounds s)

Tactic:
hs.mono (subset_upperBounds_lowerBounds s)

Premises used: BddAbove, Set.Nonempty.mono, subset_upperBounds_lowerBounds
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLeast s a
⊢ IsGLB s a

Tactic:
⟨h.2, fun _ hb => hb h.1⟩

Premises used: IsGreatest, And.right, And.left, IsGLB, And.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLUB s a
⊢ upperBounds s = Ici a

Tactic:
Set.ext fun _ => ⟨fun hb => h.2 hb, fun hb => upperBounds_mono_mem hb h.1⟩

Premises used: Set.ext, upperBounds_mono_mem, And.right, And.left, Iff.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLeast s a
⊢ lowerBounds s = Iic a

Tactic:
h.isGLB.lowerBounds_eq

Premises used: IsLeast.isGLB, IsGLB.lowerBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : IsGreatest s a
⊢ a < b ↔ ∀ x ∈ s, x < b

Tactic:
⟨fun hlt _x hx => (h.2 hx).trans_lt hlt, fun h' => h' _ h.1⟩

Premises used: And.right, And.left, Iff.intro, LE.le.trans_lt
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : IsLUB s a
rw : a ≤ b ↔ b ∈ Ici a
⊢ a ≤ b ↔ b ∈ upperBounds s

Tactic:
rw [h.upperBounds_eq]

Premises used: IsLUB.upperBounds_eq
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a

Tactic:
rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
⊢ IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s

Tactic:
⟨fun h _ => isLUB_le_iff h, fun H => ⟨(H _).1 le_rfl, fun b hb => (H b).2 hb⟩⟩

Premises used: Iff.mpr, le_rfl, isLUB_le_iff, And.intro, Iff.intro, Iff.mp
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLUB s a
⊢ BddAbove s

Tactic:
⟨a, h.1⟩

Premises used: BddAbove, Set.Nonempty, And.left, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsGreatest s a
⊢ BddAbove s

Tactic:
⟨a, h.2⟩

Premises used: BddAbove, Set.Nonempty, And.right, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
h : IsLeast s a
⊢ s.Nonempty

Tactic:
⟨a, h.1⟩

Premises used: Set.Nonempty, And.left, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
⊢ upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t

Tactic:
Subset.antisymm (fun _ hb => ⟨fun _ hx => hb (Or.inl hx), fun _ hx => hb (Or.inr hx)⟩)
    fun _ hb _ hx => hx.elim (fun hs => hb.1 hs) fun ht => hb.2 ht

Premises used: Set.Subset.antisymm, And.right, And.left, And.intro, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
⊢ upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)

Tactic:
union_subset (upperBounds_mono_set inter_subset_left)
    (upperBounds_mono_set inter_subset_right)

Premises used: upperBounds_mono_set, Set.inter_subset_left, Set.union_subset, Set.inter_subset_right
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
a : α
s t : Set α
⊢ IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a

Tactic:
simp [IsLeast, lowerBounds_union, or_and_right, and_comm (a := a ∈ t), and_assoc]

Premises used: lowerBounds_union, and_comm, IsLeast, and_assoc, or_and_right
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : BddAbove s
⊢ BddAbove (s ∩ t)

Tactic:
h.mono inter_subset_left

Premises used: Set.inter_subset_left, BddAbove.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : BddAbove t
⊢ BddAbove (s ∩ t)

Tactic:
h.mono inter_subset_right

Premises used: Set.inter_subset_right, BddAbove.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
obtain : ∀ (c : α) (hca : a ≤ c) (hcb : b ≤ c), BddAbove (s ∪ t)
⊢ BddAbove (s ∪ t)

Tactic:
obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
rw : (upperBounds s ∩ upperBounds t).Nonempty
⊢ BddAbove (s ∪ t)

Tactic:
rw [BddAbove, upperBounds_union]

Premises used: BddAbove, upperBounds_union
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds s ∩ upperBounds t).Nonempty

Tactic:
⟨c, upperBounds_mono_mem hca ha, upperBounds_mono_mem hcb hb⟩

Premises used: upperBounds_mono_mem, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds s ∩ upperBounds t).Nonempty

Tactic:
exact ⟨c, upperBounds_mono_mem hca ha, upperBounds_mono_mem hcb hb⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s t : Set α
⊢ BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t

Tactic:
⟨fun h => ⟨h.mono subset_union_left, h.mono subset_union_right⟩, fun h =>
    h.1.union h.2⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, BddAbove.union, BddAbove.mono
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
have : ∀ (af : α) (haf : af ∈ upperBounds (range f)), BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
⊢ BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)

Tactic:
have ⟨af, haf⟩ := hf
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
af : α
haf : af ∈ upperBounds (range f)
have : ∀ (ag : α) (hag : ag ∈ upperBounds (range g)), BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
⊢ BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)

Tactic:
have ⟨ag, hag⟩ := hg
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
af : α
haf : af ∈ upperBounds (range f)
ag : α
hag : ag ∈ upperBounds (range g)
⊢ BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)

Tactic:
⟨af ⊔ ag, fun a ⟨i, ha⟩ ↦ ha ▸ sup_le_sup (haf ⟨i, rfl⟩) (hag ⟨i, rfl⟩)⟩

Premises used: sup_le_sup, Eq.rec, LE.le, BddAbove, Set.Nonempty, Max.max, Exists.intro, _private.0.bbdAbove_range_sup.match_2, rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
af : α
haf : af ∈ upperBounds (range f)
ag : α
hag : ag ∈ upperBounds (range g)
⊢ BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)

Tactic:
exact ⟨af ⊔ ag, fun a ⟨i, ha⟩ ↦ ha ▸ sup_le_sup (haf ⟨i, rfl⟩) (hag ⟨i, rfl⟩)⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
have : ∀ (b : α) (hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b), BddAbove (range f)
⊢ BddAbove (range f)

Tactic:
have ⟨b, hb⟩ := h
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
b : α
hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b
⊢ BddAbove (range f)

Tactic:
⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_left.trans (hb ⟨i, rfl⟩)⟩

Premises used: le_sup_left, Eq.rec, LE.le, BddAbove, Set.Nonempty, _private.0.bbdAbove_range_left_of_sup.match_2, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
b : α
hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b
⊢ BddAbove (range f)

Tactic:
exact ⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_left.trans (hb ⟨i, rfl⟩)⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
have : ∀ (b : α) (hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b), BddAbove (range g)
⊢ BddAbove (range g)

Tactic:
have ⟨b, hb⟩ := h
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
b : α
hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b
⊢ BddAbove (range g)

Tactic:
⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_right.trans (hb ⟨i, rfl⟩)⟩

Premises used: Eq.rec, le_sup_right, LE.le, BddAbove, Set.Nonempty, _private.0.bbdAbove_range_left_of_sup.match_2, Exists.intro, LE.le.trans, rfl
-- Module: Mathlib.Order.Bounds.Basic
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
b : α
hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b
⊢ BddAbove (range g)

Tactic:
exact ⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_right.trans (hb ⟨i, rfl⟩)⟩
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : SemilatticeSup γ
a b : γ
s t : Set γ
hs : IsLUB s a
ht : IsLUB t b
⊢ IsLUB (s ∪ t) (a ⊔ b)

Tactic:
⟨fun _ h =>
    h.casesOn (fun h => le_sup_of_le_left <| hs.left h) fun h => le_sup_of_le_right <| ht.left h,
    fun _ hc =>
    sup_le (hs.right fun _ hd => hc <| Or.inl hd) (ht.right fun _ hd => hc <| Or.inr hd)⟩

Premises used: Or.casesOn, IsLeast, And.right, And.intro, IsLUB, sup_le, Or.inl, Or.inr
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
inl : ∀ (h : a ≤ b), min a b ∈ s ∪ t
inr : ∀ (h : b ≤ a), min a b ∈ s ∪ t
⊢ min a b ∈ s ∪ t

Tactic:
rcases le_total a b with h | h

Premises used: le_total
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : a ≤ b
⊢ min a b ∈ s ∪ t

Tactic:
simp [h, ha.1, hb.1]

Premises used: And.left
-- Module: Mathlib.Order.Bounds.Basic
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : b ≤ a
⊢ min a b ∈ s ∪ t

Tactic:
simp [h, ha.1, hb.1]

Premises used: And.left