awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
ι : Sort u_1
α : Type u_2
inst : LE α
P : ι → Prop
f : ι → α
i : ι
h : MinimalFor P f i
⊢ P i

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
ι : Sort u_1
α : Type u_2
inst : LE α
P : ι → Prop
f : ι → α
i j : ι
h : MinimalFor P f i
hj : P j
hji : f j ≤ f i
⊢ f i ≤ f j

Tactic:
h.2 hj hji

Premises used: And.right
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
a b : α
⊢ r a b ↔ r b a

Tactic:
⟨symm, symm⟩

Premises used: Iff.intro, symm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Antisymm r
a b : α
⊢ r a b → r b a → b = a

Tactic:
fun h h' => antisymm h' h

Premises used: antisymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : Std.Antisymm r
a : α
⊢ r a a ∧ r a a

Tactic:
⟨refl _, refl _⟩

Premises used: And.intro, refl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : Std.Antisymm r
a : α
⊢ r a a ∧ r a a

Tactic:
exact ⟨refl _, refl _⟩
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Antisymm r
a b : α
⊢ r a b → r b a → a = b

Tactic:
antisymm

Premises used: antisymm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Antisymm r
a b : α
⊢ r a b → r b a → b = a

Tactic:
antisymm'

Premises used: antisymm'
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
a b : α
⊢ r a b ↔ r b a

Tactic:
comm

Premises used: comm
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Asymm r
⊢ Antisymm r

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Asymm r
⊢ Irrefl r

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Total r
⊢ Trichotomous r

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
β : Sort u_2
r_1 : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst : Total r
⊢ Refl r

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Irrefl r
inst_1 : Subsingleton α
x y : α
⊢ ¬r x y

Tactic:
Subsingleton.elim x y ▸ irrefl x

Premises used: irrefl, Eq.rec, Subsingleton.elim
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : Subsingleton α
x y : α
⊢ r x y

Tactic:
Subsingleton.elim x y ▸ refl x

Premises used: Eq.rec, Subsingleton.elim, refl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
a b : α
⊢ emptyRelation a b ↔ False

Tactic:
Iff.rfl

Premises used: Iff.rfl, emptyRelation
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
s : β → β → Prop
⊢ Std.Irrefl.{u_1} (α := α) emptyRelation

Tactic:
⟨fun _ => id⟩

Premises used: id, Std.Irrefl.mk
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
inst_1 : IsTrans α r
a b c : α
h : r a b
⊢ r a c ↔ r b c

Tactic:
⟨trans_of r (symm_of r h), trans_of r h⟩

Premises used: symm_of, Iff.intro, trans_of
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
inst_1 : IsTrans α r
a b c : α
h : r b c
⊢ r a b ↔ r a c

Tactic:
⟨(trans_of r · h), (trans_of r · (symm_of r h))⟩

Premises used: symm_of, Iff.intro, trans_of
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
inst_1 : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
rw : r b c ↔ r b d
rw₁ rw₂ : r b d ↔ r b d
⊢ r a c ↔ r b d

Tactic:
rw [rel_congr_left h₁, rel_congr_right h₂]

Premises used: rel_congr_left, rel_congr_right
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
inl : ∀ (h₃ : r a b), r a c
inr : ∀ (h₁ : ¬r a a) (h₂ : r a c), r a c
inr₁ : ∀ (h₃ : r b a), r a c
⊢ r a c

Tactic:
rcases trichotomous_of r a b with (h₃ | rfl | h₃)

Premises used: trichotomous_of, rfl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

Tactic:
_root_.trans h₃ h₂

Premises used: trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

Tactic:
exact _root_.trans h₃ h₂

Premises used: trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

Tactic:
h₂
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

Tactic:
exact h₂
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
absurd h₃ h₁

Premises used: absurd
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
exact absurd h₃ h₁

Premises used: absurd
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
inl : ∀ (h₃ : r b c), r a c
inr : ∀ (h₂ : ¬r b b), r a b
inr₁ : ∀ (h₃ : r c b), r a c
⊢ r a c

Tactic:
rcases trichotomous_of r b c with (h₃ | rfl | h₃)

Premises used: trichotomous_of, rfl
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

Tactic:
_root_.trans h₁ h₃

Premises used: trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

Tactic:
exact _root_.trans h₁ h₃

Premises used: trans
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

Tactic:
h₁
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

Tactic:
exact h₁
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
absurd h₃ h₂

Premises used: absurd
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
exact absurd h₃ h₂

Premises used: absurd
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
⊢ Transitive r

Tactic:
IsTrans.trans

Premises used: IsTrans.trans, Transitive
-- Module: Mathlib.Order.Defs.Unbundled
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Trichotomous r
inst_1 : Std.Irrefl r
a b : α
H : ∀ (x : α), r x a ↔ r x b
⊢ a = b

Tactic:
((@trichotomous _ r _ a b).resolve_left <| mt (H _).2 <| irrefl a).resolve_right <| mt (H _).1
    <| irrefl b

Premises used: Iff.mpr, irrefl, mt, Or.resolve_left, Iff.mp, trichotomous, Or.resolve_right
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
⊢ DirSupClosedOn univ s ↔ DirSupClosed s

Tactic:
simp [DirSupClosedOn, DirSupClosed]

Premises used: DirSupClosed, DirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
⊢ DirSupInaccOn univ s ↔ DirSupInacc s

Tactic:
simp [DirSupInaccOn, DirSupInacc]

Premises used: DirSupInacc, DirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
⊢ DirSupClosed s → DirSupClosedOn D s

Tactic:
@fun h _ _ ↦ @h _

Premises used: DirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
⊢ DirSupInacc s → DirSupInaccOn D s

Tactic:
@fun h _ _ ↦ @h _

Premises used: DirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsEmpty α
s : Set α
⊢ DirSupClosed s

Tactic:
fun _ _ ⟨a, _⟩ ↦ isEmptyElim a

Premises used: _private.0.DirSupClosed.of_isEmpty.match_1, isEmptyElim, DirSupClosed
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsEmpty α
s : Set α
⊢ DirSupInacc s

Tactic:
fun _ ⟨a, _⟩ ↦ isEmptyElim a

Premises used: _private.0.DirSupClosed.of_isEmpty.match_1, isEmptyElim, DirSupInacc
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : IsEmpty α
s : Set α
⊢ DirSupClosedOn D s

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
inst_1 : IsEmpty α
s : Set α
⊢ DirSupInaccOn D s

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D₁ D₂ : Set (Set α)
inst : Preorder α
hD : D₁ ⊆ D₂
hf : DirSupClosedOn D₂ s
⊢ DirSupClosedOn D₁ s

Tactic:
fun _ a ↦ hf (hD a)

Premises used: DirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D₁ D₂ : Set (Set α)
inst : Preorder α
hD : D₁ ⊆ D₂
hf : DirSupInaccOn D₂ s
⊢ DirSupInaccOn D₁ s

Tactic:
fun _ a ↦ hf (hD a)

Premises used: DirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
simp_rw :
  (∀ ⦃d : Set α⦄,
      d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ¬Disjoint d s
⊢ DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s

Tactic:
simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter]

Premises used: Set.not_disjoint_iff_nonempty_inter, DirSupClosedOn, DirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
⊢ (∀ ⦃d : Set α⦄,
      d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ¬Disjoint d s

Tactic:
grind
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
rw : DirSupClosedOn univ sᶜ ↔ DirSupInacc s
rw₁ : DirSupInaccOn univ s ↔ DirSupInacc s
rw₂ rw₃ : DirSupInacc s ↔ DirSupInacc s
⊢ DirSupClosed sᶜ ↔ DirSupInacc s

Tactic:
rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ]

Premises used: dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
rw : DirSupClosedOn D sᶜᶜ ↔ DirSupClosedOn D s
rw₁ rw₂ : DirSupClosedOn D s ↔ DirSupClosedOn D s
⊢ DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s

Tactic:
rw [← dirSupClosedOn_compl, compl_compl]

Premises used: compl_compl, dirSupClosedOn_compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s : Set α
inst : Preorder α
rw : DirSupClosed sᶜᶜ ↔ DirSupClosed s
rw₁ rw₂ : DirSupClosed s ↔ DirSupClosed s
⊢ DirSupInacc sᶜ ↔ DirSupClosed s

Tactic:
rw [← dirSupClosed_compl, compl_compl]

Premises used: compl_compl, dirSupClosed_compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
⊢ DirSupClosed.{u_1} (α := α) ∅

Tactic:
simp [DirSupClosed]

Premises used: DirSupClosed
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
⊢ DirSupInacc.{u_1} (α := α) ∅

Tactic:
simp [DirSupInacc]

Premises used: DirSupInacc
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
⊢ DirSupClosedOn D ∅

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
⊢ DirSupInaccOn D ∅

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
⊢ DirSupClosed.{u_1} (α := α) Set.univ

Tactic:
simp [DirSupClosed]

Premises used: DirSupClosed
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
⊢ DirSupInacc.{u_1} (α := α) Set.univ

Tactic:
simp [← compl_empty]

Premises used: Set.compl_empty
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
⊢ DirSupClosedOn D Set.univ

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
⊢ DirSupInaccOn D Set.univ

Tactic:
simp
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupClosedOn D x
⊢ DirSupClosedOn D (⋂₀ s)

Tactic:
fun _d hD hds hd hd' _a ha t ht ↦ hs t ht hD (hds.trans fun _x hx ↦ hx _ ht) hd hd' ha

Premises used: Set.Mem, setOf, HasSubset.Subset.trans, DirSupClosedOn, Set.sInter
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupClosed x
⊢ DirSupClosed (⋂₀ s)

Tactic:
simpa using DirSupClosedOn.sInter fun x hx ↦ (hs x hx).dirSupClosedOn (D := .univ)

Premises used: DirSupClosedOn.sInter, DirSupClosed.dirSupClosedOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
rw : DirSupClosedOn D (⋂₀ (Compl.compl '' s))
⊢ DirSupInaccOn D (⋃₀ s)

Tactic:
rw [← dirSupClosedOn_compl, Set.compl_sUnion]

Premises used: Set.compl_sUnion, dirSupClosedOn_compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
hs₁ : ∀ x ∈ Compl.compl '' s, DirSupClosedOn D x
⊢ DirSupClosedOn D (⋂₀ (Compl.compl '' s))

Tactic:
apply DirSupClosedOn.sInter

Premises used: DirSupClosedOn.sInter
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
x : Set α
hx : x ∈ s
⊢ DirSupClosedOn D xᶜ

Tactic:
(hs x hx).compl

Premises used: DirSupInaccOn.compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
x : Set α
hx : x ∈ s
⊢ DirSupClosedOn D xᶜ

Tactic:
exact (hs x hx).compl

Premises used: DirSupInaccOn.compl
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInacc x
⊢ DirSupInacc (⋃₀ s)

Tactic:
simpa using DirSupInaccOn.sUnion fun x hx ↦ (hs x hx).dirSupInaccOn (D := .univ)

Premises used: DirSupInaccOn.sUnion, DirSupInacc.dirSupInaccOn
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ ∀ x ∈ range f, DirSupClosedOn D x

Tactic:
simpa
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ DirSupClosedOn D (⋂₀ range f)

Tactic:
exact DirSupClosedOn.sInter (by simpa)

Premises used: DirSupClosedOn.sInter
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ ∀ x ∈ range f, DirSupClosed x

Tactic:
simpa
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ DirSupClosed (⋂₀ range f)

Tactic:
exact DirSupClosed.sInter (by simpa)

Premises used: DirSupClosed.sInter
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ ∀ x ∈ range f, DirSupInaccOn D x

Tactic:
simpa
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ DirSupInaccOn D (⋃₀ range f)

Tactic:
exact DirSupInaccOn.sUnion (by simpa)

Premises used: DirSupInaccOn.sUnion
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ ∀ x ∈ range f, DirSupInacc x

Tactic:
simpa
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ DirSupInacc (⋃₀ range f)

Tactic:
exact DirSupInacc.sUnion (by simpa)

Premises used: DirSupInacc.sUnion
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
rw : DirSupClosedOn D (⋂₀ {s, t})
⊢ DirSupClosedOn D (s ∩ t)

Tactic:
rw [← sInter_pair]

Premises used: Set.sInter_pair
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (⋂₀ {s, t})

Tactic:
.sInter ?_

Premises used: DirSupClosedOn.sInter
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
refine : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → DirSupClosedOn D x
⊢ DirSupClosedOn D (⋂₀ {s, t})

Tactic:
refine .sInter ?_
-- Module: Mathlib.Order.DirSupClosed
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → DirSupClosedOn D x

Tactic:
simpa [hs]
-- 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.inter ht.dirSupClosedOn (D := .univ)

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

Tactic:
rw [← dirSupClosedOn_compl, compl_union]

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

Tactic:
hs.compl.inter ht.compl

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

Tactic:
exact hs.compl.inter ht.compl

Premises used: DirSupInaccOn.compl, DirSupClosedOn.inter
-- 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.union ht.dirSupInaccOn (D := .univ)

Premises used: DirSupInaccOn.union, DirSupInacc.dirSupInaccOn
-- 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 : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ d ∩ s ∪ d ∩ t = d

Tactic:
grind
-- 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 : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ d ∩ s ∪ d ∩ t = d

Tactic:
have hdst : d ∩ s ∪ d ∩ t = d := by grind
-- 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 : 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
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
⊢ a ∈ s ∪ t

Tactic:
rw [← hdst] at hd₀ hd₁
-- 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 : 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
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
⊢ a ∈ s ∪ t

Tactic:
wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty

Premises used: DirectedOn, LE.le, Inter.inter, Set.Nonempty
-- 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 : 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)
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
⊢ a ∈ s ∪ t

Tactic:
rw [union_comm] at hdu hd₀ hd₁ hdst ⊢

Premises used: Set.union_comm