awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∪ t)
have rw : DirSupClosedOn D (sᶜ ∩ tᶜ)
Tactic: rw [← dirSupClosedOn_compl, compl_union]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
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 : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ a ∈ s ∪ t
have hdst : d ∩ s ∪ d ∩ t = d
Tactic: have hdst : d ∩ s ∪ d ∩ t = d := by grind
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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 : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
⊢ a ∈ s ∪ t
have rw : ∀ (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), a ∈ s ∪ t
Tactic: rw [← hdst] at hd₀ hd₁
Cleared hypotheses: hd₀, hd₁, a, ha, hdst
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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 : 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
⊢ a ∈ s ∪ t
have inr : ∀
  (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 ∈ s ∪ t
Tactic: wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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 : 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
inr :
  ∀
    (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 ∈ s ∪ t
⊢ a ∈ s ∪ t
have wlog : ∀ {α : 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
Tactic: wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty
Cleared hypotheses: hDL, hs, ht, d, hD, hdu, hd₀, hd₁, a, ha, hdst
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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 : 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
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 ∈ s ∪ t
have inr : ∀ (hdu : d ⊆ t ∪ s) (hd₀ : (d ∩ s ∪ d ∩ t).Nonempty) (hd₀ : (d ∩ t ∪ d ∩ s).Nonempty)
  (hd₁ : 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 : 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: rw [union_comm] at hdu hd₀ hd₁ hdst ⊢
Cleared hypotheses: hd₀, hd₁, a, ha, hdst, this, h
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
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
⊢ a ∈ s ∪ t
have hds : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (d ∩ s)
Tactic: obtain ⟨hds, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
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)
⊢ a ∈ s ∪ t
have hn : (d ∩ s).Nonempty
Tactic: obtain ⟨hds, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ a ∈ s ∪ t
have pos : ∀ (had : a ∈ lowerBounds (upperBounds (d ∩ s))), a ∈ s ∪ t
Tactic: by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s))
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ a ∈ s ∪ t
have neg : ∀ (had : a ∉ lowerBounds (upperBounds (d ∩ s))), a ∈ s ∪ t
Tactic: by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s))
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
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
have had₁ : ∃ (x : α) (_ : x ∈ upperBounds (d ∩ s)), ¬a ≤ x
Tactic: simp only [lowerBounds, mem_setOf_eq, not_forall] at had
Cleared hypotheses: had
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ a ∈ s ∪ t
have neg : ∀ (b : α) (hb : b ∈ upperBounds (d ∩ s)) (hb' : ¬a ≤ b), a ∈ s ∪ t
Tactic: obtain ⟨b, hb, hb'⟩ := had
Cleared hypotheses: had
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
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
⊢ a ∈ s ∪ t
have key : {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⟩⟩
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ Set.Nonempty.{u_1} (α := α) {x : α | x ∈ d ∧ ¬x ≤ b}
have contrapose! : ∀ (hb' : Eq.{u_1 + 1} (α := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} ∅), a ≤ b
Tactic: contrapose! hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
have a₁ : b ∈ upperBounds d
Tactic: apply ha.2
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ a ∈ s ∪ t
have neg : ∀ (w : α) (hw : Membership.mem (γ := Set α) {x : α | x ∈ d ∧ ¬x ≤ b} w), a ∈ s ∪ t
Tactic: obtain ⟨w, hw⟩ : {x ∈ d | ¬ x ≤ b}.Nonempty := by
      contrapose! hb'
      apply ha.2
      aesop
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
have 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
Tactic: refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right)
      ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ a ∈ s ∪ t
have neg₁ : IsLUB (d ∩ fun (x : α) ↦ x ≤ b → False) a
Tactic: refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right)
      ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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 ∈ d ∩ fun (x : α) ↦ x ≤ b → False, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have 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
Tactic: obtain ⟨z, hz, hz'⟩ := hd₁ _ (.inr (key hx)) _ (.inr (key hy))
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
have neg : ∀ (x : α) (hx : x ∈ upperBounds (d ∩ fun (x : α) ↦ x ≤ b → False)) (y : α) (hy : y ∈ d), y ≤ x
Tactic: refine ⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ y ≤ x
have pos : ∀ (hyb : y ≤ b), y ≤ x
Tactic: by_cases hyb : y ≤ b
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
⊢ y ≤ x
have neg : ∀ (hyb : ¬y ≤ b), y ≤ x
Tactic: by_cases hyb : y ≤ b
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
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
have pos : ∀ (z : α) (hz : z ∈ d ∩ s ∪ d ∩ t) (hxz : y ≤ z) (hyz : w ≤ z), y ≤ x
Tactic: obtain ⟨z, hz, hxz, hyz⟩ := hd₁ _ (hdst ▸ hy) _ (.inr (key hw))
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupInaccOn D (s ∩ t)
have rw : DirSupClosedOn D (sᶜ ∪ tᶜ)
Tactic: rw [← dirSupClosedOn_compl, compl_inter]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
hd₃ : a ∈ s
⊢ (d ∩ s).Nonempty
have obtain : ∀ (b : α) (hbd : b ∈ d) (hb : Ici b ∩ d ⊆ s), (d ∩ s).Nonempty
Tactic: obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
⊢ ∃ b ∈ t, Ici b ∩ t ⊆ s
have by_contra! : ∀ (H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
⊢ False
have H₁ : ∀ (b : (↑t : Type u_1)), ∃ (c : α), (↑b : α) ≤ c ∧ c ∈ t ∧ c ∉ s
Tactic: have H : ∀ b : t, ∃ c, b.1 ≤ c ∧ c ∈ t ∧ c ∉ s := by simpa [not_subset, and_assoc] using H
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H_1 : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
H : ∀ (b : (↑t : Type u_1)), ∃ (c : α), (↑b : α) ≤ c ∧ c ∈ t ∧ c ∉ s
⊢ False
have choose : ∀ (f : (b : (↑t : Type u_1)) → α) (hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s), False
Tactic: choose f hf using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
⊢ False
have this : Nonempty.{u_1 + 1} (↑t : Type u_1)
Tactic: have := ht₀.to_subtype
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (hypothesis)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
this : Nonempty.{u_1 + 1} (↑t : Type u_1)
⊢ False
have hft : range f ⊆ t
Tactic: have hft : range f ⊆ t := by grind
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
this : Nonempty.{u_1 + 1} (↑t : Type u_1)
hft : range f ⊆ t
⊢ False
have apply : range f ∩ s = ∅
Tactic: apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s
f : (b : (↑t : Type u_1)) → α
hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s
this : Nonempty.{u_1 + 1} (↑t : Type u_1)
hft : range f ⊆ t
apply : range f ∩ s = ∅
⊢ False
have apply₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range f)
Tactic: apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty