awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have obtain : ∀ (w : α) (hw : w ∈ s) (hzw : z ≤ w), ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
Tactic: obtain ⟨w, hw, hzw⟩ := hc hz
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
⊢ IsCofinalFor t s ∨ IsCofinalFor s t
have rw : ¬IsCofinalFor t s → IsCofinalFor s t
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
hts : ¬IsCofinalFor t s
x : α
hx : x ∈ s
⊢ ∃ b ∈ t, x ≤ b
have hts₁ : ∃ (x : α) (_ : x ∈ t), ∀ x_1 ∈ s, ¬x ≤ x_1
Tactic: simp only [IsCofinalFor, not_forall, not_exists, not_and] at hts
Cleared hypotheses: hts
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
hts : ∃ (x : α) (_ : x ∈ t), ∀ x_1 ∈ s, ¬x ≤ x_1
⊢ ∃ b ∈ t, x ≤ b
have obtain : ∀ (y : α) (hy : y ∈ t) (hys : ∀ x ∈ s, ¬y ≤ x), ∃ b ∈ t, x ≤ b
Tactic: obtain ⟨y, hy, hys⟩ := hts
Cleared hypotheses: hts
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
⊢ ∃ b ∈ t, x ≤ b
have inl : ∀ (z : α) (hzs : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ t, x ≤ b
Tactic: obtain ⟨z, (hzs | hzt), hxz, hyz⟩ := h x (.inl hx) y (.inr hy)
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hys : ∀ x ∈ s, ¬y ≤ x
inl : ∀ (z : α) (hzs : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ t, x ≤ b
⊢ ∃ b ∈ t, x ≤ b
have inr : ∀ (z : α) (hzt : z ∈ t) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ t, x ≤ b
Tactic: obtain ⟨z, (hzs | hzt), hxz, hyz⟩ := h x (.inl hx) y (.inr hy)
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
⊢ 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
have refine_1 : ∀ (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: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
refine_1 :
  ∀ (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
⊢ 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
have refine_2 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t →
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
have refine_1 : ∀ (hts : IsCofinalFor t s),
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
Tactic: rcases isCofinalFor_or_isCofinalFor_of_directedOn_union h with hts | hst
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
refine_1 :
  ∀ (hts : IsCofinalFor t s),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
      DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
have refine_1₁ : ∀ (hst : IsCofinalFor s t),
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ IsCofinalFor s t
Tactic: rcases isCofinalFor_or_isCofinalFor_of_directedOn_union h with hts | hst
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have refine_2 : ∀ (x' : α) (hx' : x' ∈ s) (hxx' : x ≤ x'),
  ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
Tactic: obtain ⟨x', hx', hxx'⟩ := hts.union_right hx
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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'
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have 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
Tactic: obtain ⟨y', hy', hyy'⟩ := hts.union_right hy
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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 ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have 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
Tactic: obtain ⟨z, hz, hx'z, hy'z⟩ := hs x' hx' y' hy'
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have 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
Tactic: obtain ⟨x', hx', hxx'⟩ := hst.union_left hx
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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'
⊢ ∃ z ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have 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
Tactic: obtain ⟨y', hy', hyy'⟩ := hst.union_left hy
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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 ∈ s ∪ t, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have 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
Tactic: obtain ⟨z, hz, hx'z, hy'z⟩ := ht x' hx' y' hy'
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (hypothesis)
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 ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
have 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
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
have 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
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
have 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
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
have 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
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
have 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
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hn : (s ∪ t).Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∪ t)
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
have 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
Tactic: obtain h | h := directedOn_or_directedOn_of_union h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
have 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
Tactic: obtain h | h := directedOn_or_directedOn_of_union h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
have 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
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s, hn, h_1, h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
have inl₁ : ∀ (hs : s.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
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
have 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} (α := α) ∅
Tactic: obtain rfl | ht := t.eq_empty_or_nonempty
Cleared hypotheses: t, hn, h_1, h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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} (α := α) ∅
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Nonempty ∨ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t ∧ t.Nonempty
have inr₁ : ∀ (ht : 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
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s
have rw : a ≤ b ↔ b ∈ Ici a
Tactic: rw [h.upperBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
⊢ BddAbove (s ∪ t)
have obtain : ∀ (c : α) (hca : a ≤ c) (hcb : b ≤ c), BddAbove (s ∪ t)
Tactic: obtain ⟨c, hca, hcb⟩ := exists_ge_ge a b
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ BddAbove (s ∪ t)
have rw : (upperBounds s ∩ upperBounds t).Nonempty
Tactic: rw [BddAbove, upperBounds_union]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
have have : ∀ (af : α) (haf : af ∈ upperBounds (range f)), BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
Tactic: have ⟨af, haf⟩ := hf
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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)
⊢ BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
have have : ∀ (ag : α) (hag : ag ∈ upperBounds (range g)), BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
Tactic: have ⟨ag, hag⟩ := hg
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
⊢ BddAbove (range f)
have have : ∀ (b : α) (hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b), BddAbove (range f)
Tactic: have ⟨b, hb⟩ := h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
ι : Sort u_4
α : Type u_5
inst : SemilatticeSup α
f g : ι → α
h : BddAbove.{u_5} (α := α) (range fun (x : ι) ↦ f x ⊔ g x)
⊢ BddAbove (range g)
have have : ∀ (b : α) (hb : Membership.mem (γ := Set α) (upperBounds (range fun (x : ι) ↦ f x ⊔ g x)) b), BddAbove (range g)
Tactic: have ⟨b, hb⟩ := h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t
have inl : ∀ (h : a ≤ b), min a b ∈ s ∪ t
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ min a b ∈ s ∪ t
have inr : ∀ (h : b ≤ a), min a b ∈ s ∪ t
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : SemilatticeSup γ
s : Set γ
x₀ : γ
⊢ BddAbove s ↔ ∃ (x : γ), x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
have rw : Monotone (β := Prop) fun (x : γ) ↦ ∀ y ∈ s, y ≤ x
Tactic: rw [bddAbove_def, exists_ge_and_iff_exists]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j
have inl : ∀ (hj_eq_i : j = i), 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
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ j = i ∨ Iio i = Iic j
have inr : ∀ (hj_lt_i : j < i), 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
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j
have inr : Iio i = Iic j
Tactic: right
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
⊢ ∃ (j : γ), IsLUB (Iio i) j
have pos : ∀ (h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i), ∃ (j : γ), IsLUB (Iio i) j
Tactic: by_cases! h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
pos : ∀ (h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i), ∃ (j : γ), IsLUB (Iio i) j
⊢ ∃ (j : γ), IsLUB (Iio i) j
have neg : ∀ (h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j), ∃ (j : γ), IsLUB (Iio i) j
Tactic: by_cases! h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∃ j ∈ upperBounds (Iio i), j < i
⊢ ∃ (j : γ), IsLUB (Iio i) j
have pos : ∀ (j : γ) (hj_ub : j ∈ upperBounds (Iio i)) (hj_lt_i : j < i), ∃ (j : γ), IsLUB (Iio i) j
Tactic: obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
Cleared hypotheses: h_exists_lt
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : LinearOrder γ
i : γ
h_exists_lt : ∀ (j : γ) (_ : j ∈ upperBounds (Iio i)), i ≤ j
⊢ ∃ (j : γ), IsLUB (Iio i) j
have neg : i ∈ lowerBounds (upperBounds (Iio i))
Tactic: refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
⊢ x ≤ a
have inl : ∀ (h₁ : a = x ⊔ a), x ≤ a
Tactic: rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
⊢ x ≤ a
have inr : ∀ (h₂ : a < x ⊔ a), x ≤ a
Tactic: rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
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
have inr : ∀ (y : γ) (lty : a < y) (ylt : y < x ⊔ a), x ≤ a
Tactic: obtain ⟨y, lty, ylt⟩ := exists_between h₂