awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∩ t)

Tactic:
simpa using hs.dirSupInaccOn.inter isLowerSet_univ ht.dirSupInaccOn

Premises used: isLowerSet_univ, DirSupInaccOn.inter, DirSupInacc.dirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
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
obtain : ∀ (b : α) (hbd : b ∈ d) (hb : Ici b ∩ d ⊆ s), (d ∩ s).Nonempty
⊢ (d ∩ s).Nonempty

Tactic:
obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃
-- Module: Mathlib.Order.DirSupClosed
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
b : α
hbd : b ∈ d
hb : Ici b ∩ d ⊆ s
⊢ (d ∩ s).Nonempty

Tactic:
⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

Premises used: le_rfl, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Order.DirSupClosed
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
b : α
hbd : b ∈ d
hb : Ici b ∩ d ⊆ s
⊢ (d ∩ s).Nonempty

Tactic:
exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ ∀ ⦃d : Set α⦄,
    Membership.mem (γ := Set (Set α)) Set.univ d →
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
simpa
-- Module: Mathlib.Order.DirSupClosed
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
by_contra! : ∀ (H : ∀ (b : α) (_ : b ∈ t), ¬Ici b ∩ t ⊆ s), False
⊢ ∃ b ∈ t, Ici b ∩ t ⊆ s

Tactic:
by_contra! H
-- Module: Mathlib.Order.DirSupClosed
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
⊢ ∀ (b : (↑t : Type u_1)), ∃ (c : α), (↑b : α) ≤ c ∧ c ∈ t ∧ c ∉ s

Tactic:
simpa [not_subset, and_assoc] using H

Premises used: and_assoc, Set.not_subset
-- Module: Mathlib.Order.DirSupClosed
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
⊢ ∀ (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
-- Module: Mathlib.Order.DirSupClosed
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
choose : ∀ (f : (b : (↑t : Type u_1)) → α) (hf : ∀ (b : (↑t : Type u_1)), (↑b : α) ≤ f b ∧ f b ∈ t ∧ f b ∉ s), False
⊢ False

Tactic:
choose f hf using H
-- Module: Mathlib.Order.DirSupClosed
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
⊢ Nonempty.{u_1 + 1} (↑t : Type u_1)

Tactic:
have := ht₀.to_subtype
-- Module: Mathlib.Order.DirSupClosed
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)
⊢ range f ⊆ t

Tactic:
grind
-- Module: Mathlib.Order.DirSupClosed
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)
⊢ range f ⊆ t

Tactic:
have hft : range f ⊆ t := by grind
-- Module: Mathlib.Order.DirSupClosed
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 = ∅
apply₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range f)
apply₂ : IsLUB (range f) a
⊢ False

Tactic:
apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty

Premises used: Set.Nonempty.ne_empty, Set.range_nonempty
-- Module: Mathlib.Order.DirSupClosed
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
⊢ range f ∩ s = ∅

Tactic:
aesop
-- Module: Mathlib.Order.DirSupClosed
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_1 : α
ha_1 : IsLUB t a_1
has : a_1 ∈ 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
a : α
ha : a ∈ range f
b : α
hb : b ∈ range f
obtain :
  ∀ (c : α) (hc : c ∈ t),
    a ≤ c → b ≤ c → ∃ z ∈ range f, (fun (x1 x2 : α) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b z
⊢ ∃ z ∈ range f, (fun (x1 x2 : α) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b z

Tactic:
obtain ⟨c, hc, _, _⟩ := ht₁ _ (hft ha) _ (hft hb)
-- Module: Mathlib.Order.DirSupClosed
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_1 : α
ha_1 : IsLUB t a_1
has : a_1 ∈ 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
a : α
ha : a ∈ range f
b : α
hb : b ∈ range f
c : α
hc : c ∈ t
left : a ≤ c
right : b ≤ c
⊢ (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) : α) ≤ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∧
    f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∈ t ∧ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∉ s

Tactic:
have := hf ⟨c, hc⟩
-- Module: Mathlib.Order.DirSupClosed
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_1 : α
ha_1 : IsLUB t a_1
has : a_1 ∈ 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_1 : Nonempty.{u_1 + 1} (↑t : Type u_1)
hft : range f ⊆ t
a : α
ha : a ∈ range f
b : α
hb : b ∈ range f
c : α
hc : c ∈ t
left : a ≤ c
right : b ≤ c
this :
  (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) : α) ≤ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∧
    f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∈ t ∧ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∉ s
⊢ ∃ z ∈ range f, (fun (x1 x2 : α) ↦ x1 ≤ x2) a z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) b z

Tactic:
grind
-- Module: Mathlib.Order.DirSupClosed
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
b : α
hb : b ∈ upperBounds (range f)
c : α
hc : c ∈ t
⊢ f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) c hc) ∈ range f

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
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
⊢ IsLUB (range f) a

Tactic:
exact ⟨upperBounds_mono_set hft ha.1,
        fun b hb ↦ ha.2 fun c hc ↦ (hf ⟨c, hc⟩).1.trans (hb <| by simp)⟩
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
⊢ DirSupInacc s ↔
    ∀ ⦃d : Set α⦄,
      d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
simpa using dirSupInaccOn_iff_inter_subset isLowerSet_univ

Premises used: isLowerSet_univ, dirSupInaccOn_iff_inter_subset
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsUpperSet s
⊢ DirSupClosed s

Tactic:
fun _d hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb

Premises used: _private.0.DirSupClosed.of_isEmpty.match_1, Membership.mem, DirSupClosed, And.left
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hs : IsUpperSet s
⊢ DirSupClosedOn D s

Tactic:
hs.dirSupClosed.dirSupClosedOn

Premises used: IsUpperSet.dirSupClosed, DirSupClosed.dirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : IsLowerSet s
⊢ DirSupInacc s

Tactic:
.of_compl hs.compl.dirSupClosed

Premises used: IsUpperSet.dirSupClosed, IsLowerSet.compl, DirSupInacc.of_compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
hs : IsLowerSet s
⊢ DirSupInaccOn D s

Tactic:
.of_compl hs.compl.dirSupClosedOn

Premises used: DirSupInaccOn.of_compl, IsLowerSet.compl, IsUpperSet.dirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
ha : a ∈ s
a₁ : IsLUB {a} b
⊢ b ∈ s

Tactic:
apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton a)

Premises used: Iff.mpr, Set.singleton_subset_iff, Exists.intro, directedOn_singleton, rfl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
ha : a ∈ s
a₁ : IsLUB {a} a
⊢ IsLUB {a} b

Tactic:
rw [← isLUB_congr_of_antisymmRel h]

Premises used: isLUB_congr_of_antisymmRel
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} a

Tactic:
isLUB_singleton

Premises used: isLUB_singleton
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ IsLUB {a} a

Tactic:
exact isLUB_singleton

Premises used: isLUB_singleton
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ∈ s ↔ b ∈ s

Tactic:
⟨hs.mem_imp_of_antisymmRel h, hs.mem_imp_of_antisymmRel h.symm⟩

Premises used: DirSupClosed.mem_imp_of_antisymmRel, Iff.intro, AntisymmRel.symm
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
hs : DirSupInacc s
a b : α
h : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ∈ s ↔ b ∈ s

Tactic:
simpa [not_iff_not] using hs.compl.mem_iff_of_antisymmRel h

Premises used: not_iff_not, DirSupClosed.mem_iff_of_antisymmRel, DirSupInacc.compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ DirSupClosed (Iic a)

Tactic:
fun _d h _ _ _a ha ↦ (isLUB_le_iff ha).2 h

Premises used: Iff.mpr, Set.Mem, setOf, DirSupClosed, isLUB_le_iff, Set.Iic
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
a : α
⊢ DirSupClosedOn D (Iic a)

Tactic:
(dirSupClosed_Iic a).dirSupClosedOn

Premises used: dirSupClosed_Iic, DirSupClosed.dirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ DirSupInacc (Iic a)

Tactic:
(isLowerSet_Iic a).dirSupInacc

Premises used: IsLowerSet.dirSupInacc, isLowerSet_Iic
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
a : α
⊢ DirSupInaccOn D (Iic a)

Tactic:
(isLowerSet_Iic a).dirSupInaccOn

Premises used: IsLowerSet.dirSupInaccOn, isLowerSet_Iic
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
_ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a_2 : α⦄, IsLUB d a_2 → Membership.mem (γ := Set α) {a} a_2
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a_2 : α⦄, IsLUB d a_2 → Membership.mem (γ := Set α) {a} a_2

Tactic:
_
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
rw :
  ∀ (hda : d = {a}) (hdn : d.Nonempty),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃b : α⦄ (hb : IsLUB d b), Membership.mem (γ := Set α) {a} b
⊢ Membership.mem (γ := Set α) {a} b

Tactic:
rw [hdn.subset_singleton_iff] at hda

Premises used: Set.Nonempty.subset_singleton_iff
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ Set.Nonempty (α := α) {a}

Tactic:
subst hda
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
hdn₁ : Set.Nonempty (α := α) {a}
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) {a}

Tactic:
subst hda
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
hdn₁ : Set.Nonempty (α := α) {a}
a₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) {a}
⊢ IsLUB {a} b

Tactic:
subst hda
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hdn : Set.Nonempty (α := α) {a}
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) {a}
hb : IsLUB {a} b
⊢ Membership.mem (γ := Set α) {a} b

Tactic:
mem_singleton_of_eq (hb.unique isLUB_singleton)

Premises used: Set.mem_singleton_of_eq, isLUB_singleton, IsLUB.unique
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hdn : Set.Nonempty (α := α) {a}
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) {a}
hb : IsLUB {a} b
⊢ Membership.mem (γ := Set α) {a} b

Tactic:
exact mem_singleton_of_eq (hb.unique isLUB_singleton)

Premises used: Set.mem_singleton_of_eq, isLUB_singleton, IsLUB.unique
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : PartialOrder α
a : α
⊢ DirSupClosedOn D {a}

Tactic:
(dirSupClosed_singleton a).dirSupClosedOn

Premises used: PartialOrder.dirSupClosed_singleton, DirSupClosed.dirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : LinearOrder α
⊢ DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

Tactic:
simp [DirSupClosedOn]

Premises used: DirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
⊢ DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s

Tactic:
simp [DirSupClosed]

Premises used: DirSupClosed
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : LinearOrder α
⊢ DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInaccOn]

Premises used: DirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInacc]

Premises used: DirSupInacc
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : CompleteLattice α
⊢ DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → sSup d ∈ s

Tactic:
simp [DirSupClosedOn, isLUB_iff_sSup_eq]

Premises used: isLUB_iff_sSup_eq, DirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : CompleteLattice α
⊢ DirSupInaccOn D s ↔
    ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInaccOn, isLUB_iff_sSup_eq]

Premises used: isLUB_iff_sSup_eq, DirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : CompleteLattice α
⊢ DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → sSup d ∈ s

Tactic:
simp [DirSupClosed, isLUB_iff_sSup_eq]

Premises used: isLUB_iff_sSup_eq, DirSupClosed
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : CompleteLattice α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInacc, isLUB_iff_sSup_eq]

Premises used: isLUB_iff_sSup_eq, DirSupInacc
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
simp :
  (∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔
    ∀ (a : α) (b : a ∈ s) (a_1 : α) (b : a_1 ∈ s), ∃ (a_2 : α), r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
⊢ DirectedOn r s ↔ Directed (ι := { x : α // x ∈ s }) r (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall]

Premises used: Directed, DirectedOn, Subtype.exists, exists_and_left, Subtype.forall, exists_prop
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
x : α
h : x ∈ s
⊢ (∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔ ∀ (a : α) (b : a ∈ s), ∃ (a_1 : α), r x a_1 ∧ a_1 ∈ s ∧ r a a_1

Tactic:
simp [And.comm, and_assoc]

Premises used: And.comm, and_assoc
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ (∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z) ↔
    ∀ (a : α) (b : a ∈ s) (a_1 : α) (b : a_1 ∈ s), ∃ (a_2 : α), r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2

Tactic:
exact forall₂_congr fun x _ => by simp [And.comm, and_assoc]

Premises used: forall₂_congr
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
simp_rw : DirectedOn r (Set.range f) ↔ ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
simp_rw₁ :
  (∀ x ∈ Set.range f, ∀ y ∈ Set.range f, ∃ z ∈ Set.range f, r x z ∧ r y z) ↔
    ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
simp_rw₂ :
  (∀ (i i_1 : ι), ∃ z ∈ Set.range f, r (f i) z ∧ r (f i_1) z) ↔ ∀ (x y : ι), ∃ (z : ι), r (f x) (f z) ∧ r (f y) (f z)
⊢ DirectedOn r (Set.range f) ↔ Directed r f

Tactic:
simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]

Premises used: Set.forall_mem_range, Directed, DirectedOn, Set.exists_range_iff
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

Tactic:
simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Order.Preimage]

Premises used: and_imp, DirectedOn, Set.mem_image, forall_exists_index, exists_exists_and_eq_and, forall_apply_eq_imp_iff₂, Order.Preimage
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r r' : α → α → Prop
s : Set α
hs : DirectedOn r s
h : ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b → r' a b
⊢ DirectedOn r' s

Tactic:
fun _ hx _ hy =>
  let ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
  ⟨z, hz, h hx hz hxz, h hy hz hyz⟩

Premises used: _private.0.DirectedOn.mono'.match_1, DirectedOn, Membership.mem, Exists, And, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r r' : α → α → Prop
s : Set α
h : DirectedOn r s
H : ∀ ⦃a b : α⦄, r a b → r' a b
⊢ DirectedOn r' s

Tactic:
h.mono' fun _ _ _ _ h ↦ H h

Premises used: DirectedOn.mono'
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
ι : Sort u_5
f : ι → β
g : β → α
⊢ Directed r (g ∘ f) ↔ Directed (g ⁻¹'o r) f

Tactic:
Iff.rfl

Premises used: Directed, Iff.rfl, Order.Preimage
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
ι : Sort u_3
κ : Sort u_4
r : α → α → Prop
f : ι → κ
hf : Surjective f
g : κ → α
⊢ Directed r (g ∘ f) ↔ Directed r g

Tactic:
simp [Directed, hf.forall, hf.exists]

Premises used: Function.Surjective.forall, Function.Surjective.exists, Directed
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r s : α → α → Prop
ι : Sort u_5
f : ι → α
H : ∀ (a b : α), r a b → s a b
h : Directed r f
⊢ Directed s f

Tactic:
fun a b =>
  let ⟨c, h₁, h₂⟩ := h a b
  ⟨c, H _ _ h₁, H _ _ h₂⟩

Premises used: _private.0.Directed.mono.match_1, Directed, Exists, And, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
ι : Sort u_5
rb : β → β → Prop
g : α → β
f : ι → α
hg : ∀ ⦃x y : α⦄, r x y → rb (g x) (g y)
hf : Directed r f
⊢ Directed rb (g ∘ f)

Tactic:
directed_comp.2 <| hf.mono hg

Premises used: Iff.mpr, Directed.mono, directed_comp
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
rb : β → β → Prop
g : α → β
s : Set α
hg : ∀ ⦃x y : α⦄, r x y → rb (g x) (g y)
hf : DirectedOn r s
⊢ DirectedOn rb (g '' s)

Tactic:
directedOn_image.mpr (hf.mono hg)

Premises used: Iff.mpr, directedOn_image, DirectedOn.mono
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
⊢ ∀ ⦃x y : β⦄, (r on f) x y → r (f x) (f y)

Tactic:
simp
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
refine : ∀ (h : DirectedOn r (f '' s)) (x : β) (hx : x ∈ s) (y : β) (hy : y ∈ s), ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
⊢ DirectedOn (r on f) s ↔ DirectedOn r (f '' s)

Tactic:
refine ⟨DirectedOn.mono_comp (by simp), fun h x hx y hy ↦ ?_⟩