awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu_1 : d ⊆ s ∪ t
hdu : d ⊆ t ∪ s
hd₀_1 : (d ∩ s ∪ d ∩ t).Nonempty
hd₀ : (d ∩ t ∪ d ∩ s).Nonempty
hd₁_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ t ∪ d ∩ s)
a : α
ha : IsLUB d a
hdst_1 : d ∩ s ∪ d ∩ t = d
hdst : d ∩ t ∪ d ∩ s = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α] (hDL : IsLowerSet D) (hs : DirSupClosedOn D s)
    (ht : DirSupClosedOn D t) ⦃d : Set α⦄ (hD : d ∈ D) (hdu : d ⊆ s ∪ t) (hd₀ : (d ∩ s ∪ d ∩ t).Nonempty)
    (hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)) ⦃a : α⦄ (ha : IsLUB d a) (hdst : d ∩ s ∪ d ∩ t = d)
    (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s) ∧ (d ∩ s).Nonempty), a ∈ s ∪ t
h : ¬(DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s) ∧ (d ∩ s).Nonempty)
⊢ a ∈ t ∪ s

Tactic:
this hDL ht hs hD hdu hd₀ hd₁ ha hdst <|
      (directedOn_or_directedOn_of_union' hd₀ hd₁).resolve_right h

Premises used: directedOn_or_directedOn_of_union', Or.resolve_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu_1 : d ⊆ s ∪ t
hdu : d ⊆ t ∪ s
hd₀_1 : (d ∩ s ∪ d ∩ t).Nonempty
hd₀ : (d ∩ t ∪ d ∩ s).Nonempty
hd₁_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ t ∪ d ∩ s)
a : α
ha : IsLUB d a
hdst_1 : d ∩ s ∪ d ∩ t = d
hdst : d ∩ t ∪ d ∩ s = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α] (hDL : IsLowerSet D) (hs : DirSupClosedOn D s)
    (ht : DirSupClosedOn D t) ⦃d : Set α⦄ (hD : d ∈ D) (hdu : d ⊆ s ∪ t) (hd₀ : (d ∩ s ∪ d ∩ t).Nonempty)
    (hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)) ⦃a : α⦄ (ha : IsLUB d a) (hdst : d ∩ s ∪ d ∩ t = d)
    (h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s) ∧ (d ∩ s).Nonempty), a ∈ s ∪ t
h : ¬(DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s) ∧ (d ∩ s).Nonempty)
⊢ a ∈ t ∪ s

Tactic:
exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <|
      (directedOn_or_directedOn_of_union' hd₀ hd₁).resolve_right h

Premises used: directedOn_or_directedOn_of_union', Or.resolve_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s) ∧ (d ∩ s).Nonempty
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)

Tactic:
obtain ⟨hds, hn⟩ := h
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s) ∧ (d ∩ s).Nonempty
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
⊢ (d ∩ s).Nonempty

Tactic:
obtain ⟨hds, hn⟩ := h
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
pos : ∀ (had : a ∈ lowerBounds (upperBounds (d ∩ s))), a ∈ s ∪ t
neg : ∀ (had : a ∉ lowerBounds (upperBounds (d ∩ s))), a ∈ s ∪ t
⊢ a ∈ s ∪ t

Tactic:
by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s))

Premises used: lowerBounds, upperBounds, Inter.inter
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
had : a ∈ lowerBounds (upperBounds (d ∩ s))
⊢ a ∈ s ∪ t

Tactic:
.inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds
      ⟨fun b hb ↦ ha.1 hb.1, had⟩

Premises used: Set.union, Set.Mem, setOf, Set.inter_subset_left, And.left, And.intro, Or.inl, Set.inter_subset_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
had : a ∈ lowerBounds (upperBounds (d ∩ s))
⊢ a ∈ s ∪ t

Tactic:
exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds
      ⟨fun b hb ↦ ha.1 hb.1, had⟩

Premises used: Set.inter_subset_left, And.left, And.intro, Set.inter_subset_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
had : a ∉ lowerBounds (upperBounds (d ∩ s))
⊢ ∃ (x : α) (_ : x ∈ upperBounds (d ∩ s)), ¬a ≤ x

Tactic:
simp only [lowerBounds, mem_setOf_eq, not_forall] at had

Premises used: lowerBounds, Set.mem_setOf_eq, Classical.not_forall
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
had : ∃ (x : α) (_ : x ∈ upperBounds (d ∩ s)), ¬a ≤ x
neg : ∀ (b : α) (hb : b ∈ upperBounds (d ∩ s)) (hb' : ¬a ≤ b), a ∈ s ∪ t
⊢ a ∈ s ∪ t

Tactic:
obtain ⟨b, hb, hb'⟩ := had
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
⊢ {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t

Tactic:
have key : {x ∈ d | ¬ x ≤ b} ⊆ d ∩ t := fun a ⟨had, hab⟩ ↦
      ⟨had, (hdu had).resolve_left fun has ↦ hab <| hb ⟨had, has⟩⟩
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
contrapose! : ∀ (hb' : Eq.{u_1 + 1} (α := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} ∅), a ≤ b
⊢ Set.Nonempty.{u_1} (α := α) {x : α | x ∈ d ∧ ¬x ≤ b}

Tactic:
contrapose! hb'
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
hb' : Eq.{u_1 + 1} (α := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} ∅
a₁ : b ∈ upperBounds d
⊢ a ≤ b

Tactic:
apply ha.2

Premises used: And.right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
hb' : Eq.{u_1 + 1} (α := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} ∅
⊢ b ∈ upperBounds d

Tactic:
aesop
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
neg : ∀ (w : α) (hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w), a ∈ s ∪ t
⊢ a ∈ s ∪ t

Tactic:
obtain ⟨w, hw⟩ : {x ∈ d | ¬ x ≤ b}.Nonempty := by
      contrapose! hb'
      apply ha.2
      aesop

Premises used: setOf, Membership.mem, LE.le, And, Set.Nonempty, Not
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
⊢ a ∈ s ∪ t

Tactic:
Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right)
      ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_

Premises used: Set.union, Set.Mem, setOf, HasSubset.Subset.trans, Set.inter_subset_left, Exists.intro, Or.inr, Set.inter_subset_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
neg :
  ∀ (x : α) (hx : x ∈ d ∩ fun (x : α) ↦ x ≤ b → False) (y : α) (hy : y ∈ d ∩ fun (x : α) ↦ x ≤ b → False),
    ∃ z ∈ d ∩ fun (x : α) ↦ x ≤ b → False, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
neg₁ : IsLUB (d ∩ fun (x : α) ↦ x ≤ b → False) a
⊢ a ∈ s ∪ t

Tactic:
refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right)
      ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Exists.intro, Or.inr, Set.inter_subset_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ d ∩ fun (x : α) ↦ x ≤ b → False
y : α
hy : y ∈ d ∩ fun (x : α) ↦ x ≤ b → False
neg :
  ∀ (z : α) (hz : z ∈ d ∩ s ∪ d ∩ t) (hz' : (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z),
    ∃ z ∈ d ∩ fun (x : α) ↦ x ≤ b → False, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ d ∩ fun (x : α) ↦ x ≤ b → False, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨z, hz, hz'⟩ := hd₁ _ (.inr (key hx)) _ (.inr (key hy))

Premises used: Or.inr
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ d ∩ fun (x : α) ↦ x ≤ b → False
y : α
hy : y ∈ d ∩ fun (x : α) ↦ x ≤ b → False
z : α
hz : z ∈ d ∩ s ∪ d ∩ t
hz' : (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ d ∩ fun (x : α) ↦ x ≤ b → False, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
⟨z, ⟨⟨hdst ▸ hz, mt hz'.1.trans hx.2⟩, hz'⟩⟩

Premises used: mt, Eq.rec, And.right, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ d ∩ fun (x : α) ↦ x ≤ b → False
y : α
hy : y ∈ d ∩ fun (x : α) ↦ x ≤ b → False
z : α
hz : z ∈ d ∩ s ∪ d ∩ t
hz' : (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
⊢ ∃ z ∈ d ∩ fun (x : α) ↦ x ≤ b → False, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
exact ⟨z, ⟨⟨hdst ▸ hz, mt hz'.1.trans hx.2⟩, hz'⟩⟩
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
⊢ IsLUB (d ∩ fun (x : α) ↦ x ≤ b → False) a

Tactic:
⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩

Premises used: IsLeast, And.right, And.left, And.intro, IsLUB
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
neg : ∀ (x : α) (hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)) (y : α) (hy : y ∈ d), y ≤ x
⊢ IsLUB (d ∩ fun (x : α) ↦ x ≤ b → False) a

Tactic:
refine ⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)
y : α
hy : y ∈ d
pos : ∀ (hyb : y ≤ b), y ≤ x
neg : ∀ (hyb : ¬y ≤ b), y ≤ x
⊢ y ≤ x

Tactic:
by_cases hyb : y ≤ b
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)
y : α
hy : y ∈ d
hyb : y ≤ b
pos : ∀ (z : α) (hz : z ∈ d ∩ s ∪ d ∩ t) (hxz : y ≤ z) (hyz : w ≤ z), y ≤ x
⊢ y ≤ x

Tactic:
obtain ⟨z, hz, hxz, hyz⟩ := hd₁ _ (hdst ▸ hy) _ (.inr (key hw))

Premises used: Or.inr
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)
y : α
hy : y ∈ d
hyb : y ≤ b
z : α
hz : z ∈ d ∩ s ∪ d ∩ t
hxz : y ≤ z
hyz : w ≤ z
⊢ y ≤ x

Tactic:
hxz.trans (hx ⟨hdst ▸ hz, fun hzb ↦ hw.2 (hyz.trans hzb)⟩)

Premises used: Eq.rec, And.right, And.intro, LE.le.trans
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)
y : α
hy : y ∈ d
hyb : y ≤ b
z : α
hz : z ∈ d ∩ s ∪ d ∩ t
hxz : y ≤ z
hyz : w ≤ z
⊢ y ≤ x

Tactic:
exact hxz.trans (hx ⟨hdst ▸ hz, fun hzb ↦ hw.2 (hyz.trans hzb)⟩)

Premises used: Eq.rec, And.right, And.intro, LE.le.trans
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)
y : α
hy : y ∈ d
hyb : ¬y ≤ b
⊢ y ≤ x

Tactic:
hx ⟨hy, hyb⟩

Premises used: And.intro
-- Module: Mathlib.Order.DirSupClosed
Goal:
α_1 : Type u_1
s_1 t_1 : Set α_1
D_1 : Set (Set α_1)
inst : Preorder α_1
α : Type u_1
s t : Set α
D : Set (Set α)
inst_1 : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : (d ∩ s ∪ d ∩ t).Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s ∪ d ∩ t)
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
hn : (d ∩ s).Nonempty
b : α
hb : b ∈ upperBounds (d ∩ s)
hb' : ¬a ≤ b
key : {x : α | x ∈ d ∧ ¬x ≤ b} ⊆ d ∩ t
w : α
hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w
x : α
hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)
y : α
hy : y ∈ d
hyb : ¬y ≤ b
⊢ y ≤ x

Tactic:
exact hx ⟨hy, hyb⟩

Premises used: And.intro
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
rw : DirSupClosedOn D (sᶜ ∪ tᶜ)
⊢ DirSupInaccOn D (s ∩ t)

Tactic:
rw [← dirSupClosedOn_compl, compl_inter]

Premises used: Set.compl_inter, dirSupClosedOn_compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∪ tᶜ)

Tactic:
hs.compl.union hDL ht.compl

Premises used: DirSupInaccOn.compl, DirSupClosedOn.union
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∪ tᶜ)

Tactic:
exact hs.compl.union hDL ht.compl

Premises used: DirSupInaccOn.compl, DirSupClosedOn.union
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
hs : DirSupClosed s
ht : DirSupClosed t
⊢ DirSupClosed (s ∪ t)

Tactic:
simpa using hs.dirSupClosedOn.union isLowerSet_univ ht.dirSupClosedOn

Premises used: isLowerSet_univ, DirSupClosedOn.union, DirSupClosed.dirSupClosedOn