awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : ∀ (x : α), x ∈ (↑(⨅ a ∈ s, Ici a) : Set α) ↔ x ∈ (↑(upperClosure s) : Set α)
⊢ Eq (α := UpperSet α) (⨅ a ∈ s, Ici a) (upperClosure s)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
x : α
⊢ x ∈ (↑(⨅ a ∈ s, Ici a) : Set α) ↔ x ∈ (↑(upperClosure s) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
t : LowerSet α
⊢ lowerClosure s ≤ t ↔ s ⊆ (↑t : Set α)

Tactic:
⟨fun h ↦ subset_lowerClosure.trans <| LowerSet.coe_subset_coe.2 h,
    fun h ↦ lowerClosure_min h t.lower⟩

Premises used: Iff.mpr, LowerSet.coe_subset_coe, subset_lowerClosure, HasSubset.Subset.trans, Iff.intro, lowerClosure_min, LowerSet.lower
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ GaloisConnection (β := (UpperSet α)ᵒᵈ)
    (Function.comp (β := UpperSet α) (⇑toDual : (a : UpperSet α) → (UpperSet α)ᵒᵈ) upperClosure)
    (Function.comp (β := UpperSet α) SetLike.coe (⇑ofDual : (a : (UpperSet α)ᵒᵈ) → UpperSet α))

Tactic:
fun _s _t ↦ le_upperClosure

Premises used: le_upperClosure, GaloisConnection
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ GaloisConnection (β := LowerSet α) lowerClosure SetLike.coe

Tactic:
fun _s _t ↦ lowerClosure_le

Premises used: lowerClosure_le, GaloisConnection
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ Antitone.{u_1, u_1} (α := Set α) (β := UpperSet α) upperClosure

Tactic:
gc_upperClosure_coe.monotone_l

Premises used: gc_upperClosure_coe, Antitone, GaloisConnection.monotone_l
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ Monotone.{u_1, u_1} (α := Set α) (β := LowerSet α) lowerClosure

Tactic:
gc_lowerClosure_coe.monotone_l

Premises used: GaloisConnection.monotone_l, gc_lowerClosure_coe
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
rw : s ⊆ (↑⊤ : Set α) ↔ s = ∅
⊢ Eq (α := UpperSet α) (upperClosure s) ⊤ ↔ s = ∅

Tactic:
rw [eq_top_iff, le_upperClosure]

Premises used: eq_top_iff, le_upperClosure
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s ⊆ (↑⊤ : Set α) ↔ s = ∅

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (upperClosure ∅) ⊤

Tactic:
upperClosure_eq_top_iff.mpr rfl

Premises used: Iff.mpr, upperClosure_eq_top_iff, rfl
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
a : α
a₁ : ∀ (x : α), x ∈ (↑(upperClosure {a}) : Set α) ↔ x ∈ (↑(UpperSet.Ici a) : Set α)
⊢ Eq (α := UpperSet α) (upperClosure {a}) (UpperSet.Ici a)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
a x : α
⊢ x ∈ (↑(upperClosure {a}) : Set α) ↔ x ∈ (↑(UpperSet.Ici a) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (upperClosure univ) ⊥

Tactic:
bot_unique subset_upperClosure

Premises used: subset_upperClosure, bot_unique
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
⊢ Eq (α := UpperSet α) (upperClosure (s ∪ t)) (upperClosure s ⊓ upperClosure t)

Tactic:
(@gc_upperClosure_coe α _).l_sup

Premises used: Set.Mem, upperClosure, setOf, gc_upperClosure_coe, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
⊢ Eq (α := LowerSet α) (lowerClosure (s ∪ t)) (lowerClosure s ⊔ lowerClosure t)

Tactic:
(@gc_lowerClosure_coe α _).l_sup

Premises used: GaloisConnection.l_sup, gc_lowerClosure_coe
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
ι : Sort u_3
inst : Preorder α
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (upperClosure (⋃ (i : ι), f i)) (⨅ (i : ι), upperClosure (f i))

Tactic:
(@gc_upperClosure_coe α _).l_iSup

Premises used: iInf, Set.Mem, upperClosure, setOf, GaloisConnection.l_iSup, gc_upperClosure_coe, OrderDual, Set.iUnion
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
ι : Sort u_3
inst : Preorder α
f : ι → Set α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (lowerClosure (⋃ (i : ι), f i)) (⨆ (i : ι), lowerClosure (f i))

Tactic:
(@gc_lowerClosure_coe α _).l_iSup

Premises used: GaloisConnection.l_iSup, gc_lowerClosure_coe, Set.iUnion
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
S : Set (Set α)
simp_rw : Eq.{u_1 + 1} (α := UpperSet α) (upperClosure (⋃ i ∈ S, i)) (⨅ s ∈ S, upperClosure s)
⊢ Eq (α := UpperSet α) (upperClosure (⋃₀ S)) (⨅ s ∈ S, upperClosure s)

Tactic:
simp_rw [sUnion_eq_biUnion, upperClosure_iUnion]

Premises used: Set.sUnion_eq_biUnion, upperClosure_iUnion
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : s.OrdConnected
⊢ (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s

Tactic:
(subset_inter subset_upperClosure subset_lowerClosure).antisymm'
    fun _a ⟨⟨_b, hb, hba⟩, _c, hc, hac⟩ => h.out hb hc ⟨hba, hac⟩

Premises used: subset_lowerClosure, subset_upperClosure, _private.0.Set.OrdConnected.upperClosure_inter_lowerClosure.match_1, Membership.mem, Set.OrdConnected.out, Set.subset_inter, And.intro, HasSubset.Subset.antisymm'
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ s.OrdConnected ↔ (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s

Tactic:
⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩

Premises used: Iff.intro, Set.OrdConnected.upperClosure_inter_lowerClosure
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
refine : ∀ (h : (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s), s.OrdConnected
⊢ s.OrdConnected ↔ (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s

Tactic:
refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s
rw : ((↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α)).OrdConnected
⊢ s.OrdConnected

Tactic:
rw [← h]
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s
⊢ ((↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α)).OrdConnected

Tactic:
(UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected

Premises used: IsLowerSet.ordConnected, IsUpperSet.ordConnected, Set.OrdConnected.inter, UpperSet.upper, LowerSet.lower
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : (↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α) = s
⊢ ((↑(upperClosure s) : Set α) ∩ (↑(lowerClosure s) : Set α)).OrdConnected

Tactic:
exact (UpperSet.upper _).ordConnected.inter (LowerSet.lower _).ordConnected

Premises used: IsLowerSet.ordConnected, IsUpperSet.ordConnected, Set.OrdConnected.inter, UpperSet.upper, LowerSet.lower
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ lowerBounds (↑(upperClosure s) : Set α) = lowerBounds s

Tactic:
(lowerBounds_mono_set subset_upperClosure).antisymm
    fun _a ha _b ⟨_c, hc, hcb⟩ ↦ (ha hc).trans hcb

Premises used: _private.0.upperClosure_min.match_1, subset_upperClosure, lowerBounds_mono_set, LE.le, HasSubset.Subset.antisymm, LE.le.trans
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint (↑(upperClosure s) : Set α) t ↔ Disjoint s t

Tactic:
⟨Disjoint.mono_left subset_upperClosure, ?_⟩

Premises used: subset_upperClosure, Disjoint.mono_left, Iff.intro
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
refine : Disjoint s t → Disjoint (↑(upperClosure s) : Set α) t
⊢ Disjoint (↑(upperClosure s) : Set α) t ↔ Disjoint s t

Tactic:
refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
simp : (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t
⊢ Disjoint s t → Disjoint (↑(upperClosure s) : Set α) t

Tactic:
simp only [disjoint_left, SetLike.mem_coe, mem_upperClosure, forall_exists_index, and_imp]

Premises used: and_imp, Set.disjoint_left, forall_exists_index, SetLike.mem_coe, mem_upperClosure
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t

Tactic:
fun h a b hb hba ha ↦ h hb <| ht hba ha

Premises used: Not
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t

Tactic:
exact fun h a b hb hba ha ↦ h hb <| ht hba ha
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hs : IsLowerSet s
⊢ Disjoint s (↑(upperClosure t) : Set α) ↔ Disjoint s t

Tactic:
simpa only [disjoint_comm] using hs.disjoint_upperClosure_left

Premises used: disjoint_comm, IsLowerSet.disjoint_upperClosure_left
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ (↑(upperClosure s) : Set α) = s ↔ IsUpperSet s

Tactic:
⟨(· ▸ UpperSet.upper _), IsUpperSet.upperClosure⟩

Premises used: IsUpperSet.upperClosure, upperClosure, Eq.rec, Iff.intro, UpperSet.upper
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x ↔ x ∈ s

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩

Premises used: Eq.le, LE.le, _private.0.IsAntichain.minimal_mem_upperClosure_iff_mem.match_1, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
refine_1 : ∀ (h : Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x), x ∈ s
refine_2 :
  ∀ (h : x ∈ s) (b : α), (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) b → ∀ (hbx : b ≤ x) (a : α) (has : a ∈ s) (hab : a ≤ b), x ≤ b
⊢ Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x ↔ x ∈ s

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x
refine_1 : ∀ (a : α) (has : a ∈ s) (hax : a ≤ x), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨a, has, hax⟩ := h.prop

Premises used: Minimal.prop
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : Minimal (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) x
a : α
has : a ∈ s
hax : a ≤ x
refine_1 refine_1₁ refine_1₂ refine_1₃ : a ∈ s
⊢ x ∈ s

Tactic:
rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]

Premises used: Eq.le, Minimal.eq_of_ge, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h : x ∈ s
b : α
h_1 : (fun (x : α) ↦ ∃ a ∈ s, a ≤ x) b
hbx : b ≤ x
a : α
has : a ∈ s
hab refine_2 refine_2₁ refine_2₂ refine_2₃ : a ≤ b
⊢ x ≤ b

Tactic:
rwa [← hs.eq has h (hab.trans hbx)]

Premises used: IsAntichain.eq, LE.le.trans
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Maximal (fun (x : α) ↦ Membership.mem (γ := LowerSet α) (lowerClosure s) x) x ↔ x ∈ s

Tactic:
hs.to_dual.minimal_mem_upperClosure_iff_mem

Premises used: Set.Mem, setOf, IsAntichain.minimal_mem_upperClosure_iff_mem, IsAntichain.to_dual, Maximal, OrderDual
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
hs : ¬BddBelow s
⊢ Eq (α := UpperSet α) (upperClosure s) ⊥

Tactic:
le_bot_iff.mp fun x _ ↦ ⟨_, (not_bddBelow_iff.mp hs x).choose_spec.imp id le_of_lt⟩

Premises used: le_bot_iff, And.imp, Exists.choose_spec, le_of_lt, not_bddBelow_iff, id, Exists.intro, Iff.mp, Exists.choose
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMinOrder α
s : Set α
h₁ : Eq (α := UpperSet α) (upperClosure s) ⊥
h₂ : BddBelow s
⊢ False

Tactic:
simpa [h₁] using bddBelow_upperClosure.mpr h₂

Premises used: Iff.mpr, bddBelow_upperClosure
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
⊢ (↑(s.sdiff t) : Set α) = (↑s : Set α) \ (↑(lowerClosure t) : Set α)

Tactic:
rfl

Premises used: Set.diff, setOf, rfl
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ (↑(s.erase a) : Set α) = (↑s : Set α) \ (↑(LowerSet.Iic a) : Set α)

Tactic:
rfl

Premises used: Set.diff, setOf, rfl
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s.erase a

Tactic:
simp [sdiff, erase]

Premises used: UpperSet.erase, UpperSet.sdiff
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
⊢ s ≤ s.sdiff t

Tactic:
diff_subset

Premises used: Set.diff_subset, Set.diff, setOf
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ s ≤ s.erase a

Tactic:
diff_subset

Premises used: Set.diff_subset, Set.diff, setOf
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
⊢ s.sdiff t = s ↔ Disjoint (↑s : Set α) t

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
rw : s.sdiff {a} = s ↔ a ∉ s
⊢ s.erase a = s ↔ a ∉ s

Tactic:
rw [← sdiff_singleton]

Premises used: UpperSet.sdiff_singleton
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Tactic:
simp [-sdiff_singleton]

Premises used: UpperSet.sdiff_singleton
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
⊢ s < s.sdiff t ↔ ¬Disjoint (↑s : Set α) t

Tactic:
le_sdiff_left.lt_iff_ne'.trans UpperSet.sdiff_eq_left.not

Premises used: UpperSet.sdiff_eq_left, Iff.not, Iff.trans, UpperSet.le_sdiff_left, LE.le.lt_iff_ne'
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ s < s.erase a ↔ a ∈ s

Tactic:
le_erase.lt_iff_ne'.trans erase_eq.not_left

Premises used: UpperSet.erase_eq, Iff.not_left, UpperSet.le_erase, Iff.trans, LE.le.lt_iff_ne'
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
⊢ (s.sdiff t).sdiff t = s.sdiff t

Tactic:
SetLike.coe_injective sdiff_idem

Premises used: SetLike.coe_injective, sdiff_idem
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
⊢ (s.erase a).erase a = s.erase a

Tactic:
SetLike.coe_injective sdiff_idem

Premises used: SetLike.coe_injective, sdiff_idem
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_

Premises used: Iff.mpr, le_inf, ge_antisymm, le_upperClosure, UpperSet.le_sdiff_left
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
refine :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a),
    Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_

Premises used: Iff.mpr, le_inf, ge_antisymm, le_upperClosure, UpperSet.le_sdiff_left
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
inl :
  ∀ (hat : a ∈ t),
    Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
inr :
  ∀ (hat : a ∉ t),
    Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a

Tactic:
obtain hat | hat := em (a ∈ t)

Premises used: Membership.mem, em
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∈ t
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a

Tactic:
subset_union_right (subset_upperClosure hat)

Premises used: Set.union, subset_upperClosure, Set.Mem, setOf, Set.subset_union_right
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∈ t
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a

Tactic:
exact subset_union_right (subset_upperClosure hat)

Premises used: subset_upperClosure, Set.subset_union_right
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∉ t
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a

Tactic:
subset_union_left ⟨ha, ?_⟩

Premises used: Set.union, Set.Mem, setOf, Set.subset_union_left, And.intro
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∉ t
inr : a ∉ (↑(lowerClosure t) : Set α)
⊢ Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)) a

Tactic:
refine subset_union_left ⟨ha, ?_⟩
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∉ t
b : α
hb : b ∈ t
hab : a ≤ b
⊢ False

Tactic:
hat <| hst _ ha _ hb hab
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : Membership.mem (γ := Set α) (((⇑toDual : (a : Set α) → (Set α)ᵒᵈ) ∘ SetLike.coe) s) a
hat : a ∉ t
b : α
hb : b ∈ t
hab : a ≤ b
⊢ False

Tactic:
exact hat <| hst _ ha _ hb hab
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
rw : s.sdiff t ⊓ upperClosure t = s
rw₁ rw₂ : s = s
⊢ upperClosure t ⊓ s.sdiff t = s

Tactic:
rw [inf_comm, sdiff_inf_upperClosure hts hst]

Premises used: inf_comm, UpperSet.sdiff_inf_upperClosure
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
hts : {a} ⊆ (↑s : Set α)
hst : ∀ b ∈ s, ∀ (c : α), Membership.mem (γ := Set α) {a} c → b ≤ c → Membership.mem (γ := Set α) {a} b
⊢ s.erase a ⊓ Ici a = s

Tactic:
rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure]

Premises used: upperClosure_singleton, UpperSet.sdiff_inf_upperClosure, UpperSet.sdiff_singleton
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ {a} ⊆ (↑s : Set α)

Tactic:
simpa
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ (c : α), Membership.mem (γ := Set α) {a} c → b ≤ c → Membership.mem (γ := Set α) {a} b

Tactic:
simpa
-- Module: Mathlib.Order.UpperLower.Closure
Goal:
α : Type u_1
inst : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
rw : s.erase a ⊓ Ici a = s
rw₁ rw₂ : s = s
⊢ Ici a ⊓ s.erase a = s

Tactic:
rw [inf_comm, erase_inf_Ici ha has]

Premises used: UpperSet.erase_inf_Ici, inf_comm
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
s t : UpperSet α
h : s.carrier = t.carrier
mk :
  ∀ (carrier : Set α) (upper' : IsUpperSet carrier)
    (h : { carrier := carrier, upper' := upper' : UpperSet α }.carrier = t.carrier),
    { carrier := carrier, upper' := upper' : UpperSet α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
t : UpperSet α
carrier : Set α
upper' : IsUpperSet carrier
h : { carrier := carrier, upper' := upper' : UpperSet α }.carrier = t.carrier
mk :
  ∀ (carrier_1 : Set α) (upper'_1 : IsUpperSet carrier_1)
    (h :
      { carrier := carrier, upper' := upper' : UpperSet α }.carrier =
        { carrier := carrier_1, upper' := upper'_1 : UpperSet α }.carrier),
    { carrier := carrier, upper' := upper' : UpperSet α } = { carrier := carrier_1, upper' := upper'_1 }
⊢ { carrier := carrier, upper' := upper' : UpperSet α } = t

Tactic:
cases t
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
carrier : Set α
upper' : IsUpperSet carrier
carrier_1 : Set α
upper'_1 : IsUpperSet carrier_1
h :
  { carrier := carrier, upper' := upper' : UpperSet α }.carrier =
    { carrier := carrier_1, upper' := upper'_1 : UpperSet α }.carrier
⊢ { carrier := carrier, upper' := upper' : UpperSet α } = { carrier := carrier_1, upper' := upper'_1 }

Tactic:
congr
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (↑s : Set α) = (↑t : Set α) → s = t

Tactic:
SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ s.carrier = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ IsUpperSet (↑s : Set α)

Tactic:
s.upper'

Premises used: UpperSet.upper'
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : Set α
hs : IsUpperSet s
⊢ (↑{ carrier := s, upper' := hs : UpperSet α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : Set α
hs : IsUpperSet s
a : α
⊢ a ∈ { carrier := s, upper' := hs : UpperSet α } ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (↑s : Set α) ⊆ (↑t : Set α) ↔ t ≤ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (↑s : Set α) ⊂ (↑t : Set α) ↔ t < s

Tactic:
Iff.rfl

Premises used: Iff.rfl