awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
⊢ ∀ (c₁ c₂ : ClosureOperator α),
    (∀ (x : α), Eq (α := α) ((c₁ : (a : α) → α) x : α) ((c₂ : (a : α) → α) x : α)) → c₁ = c₂

Tactic:
DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
⊢ Monotone (α := α) (β := α) (⇑c : (a : α) → α)

Tactic:
c.monotone'

Premises used: ClosureOperator.toOrderHom, OrderHom.monotone'
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x : α
⊢ x ≤ (c : (a : α) → α) x

Tactic:
c.le_closure' x

Premises used: ClosureOperator.le_closure'
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x : α
⊢ Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((c : (a : α) → α) x : α)

Tactic:
c.idempotent' x

Premises used: ClosureOperator.idempotent'
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x : α
⊢ c.IsClosed ((c : (a : α) → α) x)

Tactic:
c.isClosed_iff.2 <| c.idempotent x

Premises used: Iff.mpr, ClosureOperator.isClosed_iff, ClosureOperator.idempotent
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x : α
⊢ c.IsClosed x → (c : (a : α) → α) x = x

Tactic:
c.isClosed_iff.1

Premises used: ClosureOperator.isClosed_iff, Iff.mp
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | c.IsClosed x} x ↔
      Membership.mem (γ := Set α) (range (ι := α) (⇑c : (a : α) → α)) x
⊢ Eq (α := Set α) {x : α | c.IsClosed x} (range (ι := α) (⇑c : (a : α) → α))

Tactic:
ext x
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
y : α
⊢ Membership.mem (α := α) (γ := Set α) {x : α | c.IsClosed x} ((c : (a : α) → α) y : α)

Tactic:
c.isClosed_closure _

Premises used: Set.Mem, setOf, ClosureOperator.isClosed_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
y : α
⊢ Membership.mem (α := α) (γ := Set α) {x : α | c.IsClosed x} ((c : (a : α) → α) y : α)

Tactic:
exact c.isClosed_closure _

Premises used: ClosureOperator.isClosed_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x : α
⊢ Membership.mem (γ := Set α) {x : α | c.IsClosed x} x ↔
    Membership.mem (γ := Set α) (range (ι := α) (⇑c : (a : α) → α)) x

Tactic:
exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x y : α
⊢ x ≤ (c : (a : α) → α) y ↔ LE.le (α := α) ((c : (a : α) → α) x : α) ((c : (a : α) → α) y : α)

Tactic:
⟨fun h ↦ c.idempotent y ▸ c.monotone h, (c.le_closure x).trans⟩

Premises used: Eq.rec, ClosureOperator.le_closure, Iff.intro, ClosureOperator.monotone, LE.le.trans, ClosureOperator.idempotent
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
rw : LE.le (α := α) ((c : (a : α) → α) x : α) ((c : (a : α) → α) y : α) ↔ x ≤ (c : (a : α) → α) y
rw₁ rw₂ : x ≤ (c : (a : α) → α) y ↔ x ≤ (c : (a : α) → α) y
⊢ (c : (a : α) → α) x ≤ y ↔ x ≤ y

Tactic:
rw [← hy.closure_eq, ← le_closure_iff]

Premises used: ClosureOperator.le_closure_iff, ClosureOperator.IsClosed.closure_eq
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : Preorder α
c : ClosureOperator α
x y : α
hxy : x ≤ y
hy : c.IsClosed y
⊢ (c : (a : α) → α) x ≤ y

Tactic:
hy.closure_le_iff.2 hxy

Premises used: Iff.mpr, ClosureOperator.IsClosed.closure_le_iff
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
x : α
⊢ c.IsClosed x ↔ (c : (a : α) → α) x ≤ x

Tactic:
⟨fun h ↦ h.closure_eq.le, fun h ↦ c.isClosed_iff.2 <| h.antisymm <| c.le_closure x⟩

Premises used: Iff.mpr, LE.le.antisymm, ClosureOperator.le_closure, Eq.le, ClosureOperator.isClosed_iff, Iff.intro, ClosureOperator.IsClosed.closure_eq
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
c₁ c₂ : ClosureOperator α
h : ∀ (x : α), c₁.IsClosed x ↔ c₂.IsClosed x
x : α
⊢ IsGLB (α := α) ({y : α | x ≤ y ∧ c₁.IsClosed y} : Set α) ((c₂ : (a : α) → α) x : α)

Tactic:
simpa [h] using c₂.closure_isGLB x

Premises used: ClosureOperator.closure_isGLB
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
a : ∀ (x : α), Eq (α := α) ((c : (a : α) → α) x : α) ((ofPred (⇑c : (a : α) → α) c.IsClosed ⋯ ⋯ ⋯ : (a : α) → α) x : α)
⊢ c = ofPred (⇑c : (a : α) → α) c.IsClosed ⋯ ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
x : α
⊢ Eq (α := α) ((c : (a : α) → α) x : α) ((ofPred (⇑c : (a : α) → α) c.IsClosed ⋯ ⋯ ⋯ : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
c : ClosureOperator α
⊢ Eq (α := α) ((c : (a : α) → α) ⊤ : α) (⊤ : α)

Tactic:
le_top.antisymm (c.le_closure _)

Premises used: LE.le.antisymm, ClosureOperator.le_closure, le_top
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
c : ClosureOperator α
⊢ c.IsClosed ⊤

Tactic:
c.isClosed_iff.2 c.closure_top

Premises used: Iff.mpr, ClosureOperator.isClosed_iff, ClosureOperator.closure_top
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : SemilatticeInf α
c : ClosureOperator α
x y : α
⊢ LE.le (α := α) ((c : (a : α) → α) (x ⊓ y) : α) ((c : (a : α) → α) x ⊓ (c : (a : α) → α) y : α)

Tactic:
c.monotone.map_inf_le _ _

Premises used: Monotone.map_inf_le, ClosureOperator.monotone
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ LE.le (α := α) ((c : (a : α) → α) x ⊔ (c : (a : α) → α) y : α) ((c : (a : α) → α) (x ⊔ y) : α)

Tactic:
c.monotone.le_map_sup _ _

Premises used: Monotone.le_map_sup, ClosureOperator.monotone
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
grw grw₁ : LE.le (α := α) ((c : (a : α) → α) (x ⊔ y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
⊢ LE.le (α := α) ((c : (a : α) → α) (x ⊔ y) : α) ((c : (a : α) → α) ((c : (a : α) → α) x ⊔ y : α) : α)

Tactic:
grw [← c.le_closure x]

Premises used: ClosureOperator.le_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
rw : Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) y ⊔ x : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)
rw₁ : Eq (α := α) ((c : (a : α) → α) (y ⊔ x) : α) ((c : (a : α) → α) (x ⊔ y) : α)
rw₂ rw₃ : Eq (α := α) ((c : (a : α) → α) (y ⊔ x) : α) ((c : (a : α) → α) (y ⊔ x) : α)
⊢ Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)

Tactic:
rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]

Premises used: ClosureOperator.closure_sup_closure_left, sup_comm
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : SemilatticeSup α
c : ClosureOperator α
x y : α
rw : Eq (α := α) ((c : (a : α) → α) (x ⊔ (c : (a : α) → α) y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
rw₁ rw₂ : Eq (α := α) ((c : (a : α) → α) (x ⊔ y) : α) ((c : (a : α) → α) (x ⊔ y) : α)
⊢ Eq (α := α) ((c : (a : α) → α) ((c : (a : α) → α) x ⊔ (c : (a : α) → α) y : α) : α) ((c : (a : α) → α) (x ⊔ y) : α)

Tactic:
rw [closure_sup_closure_left, closure_sup_closure_right]

Premises used: ClosureOperator.closure_sup_closure_right, ClosureOperator.closure_sup_closure_left
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
c : ClosureOperator α
p : α → Prop
hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)
a : α
⊢ a ≤ (fun (a : α) ↦ (⨅ (b : { b : α // a ≤ b ∧ p b }), (↑b : α) : α)) a

Tactic:
simp +contextual
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : CompleteLattice α
c : ClosureOperator α
S : Set α
H : ∀ x ∈ S, c.IsClosed x
⊢ c.IsClosed (sInf S)

Tactic:
isClosed_iff_closure_le.mpr <| le_of_le_of_eq c.monotone.map_sInf_le <|
    Eq.trans (biInf_congr (c.isClosed_iff.mp <| H · ·)) sInf_eq_iInf.symm

Premises used: Iff.mpr, le_of_le_of_eq, biInf_congr, sInf_eq_iInf, ClosureOperator.isClosed_iff, ClosureOperator.isClosed_iff_closure_le, Iff.mp, Monotone.map_sInf_le, ClosureOperator.monotone, Eq.symm, Eq.trans
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
inst : CompleteLattice α
c : ClosureOperator α
f : ι → α
⊢ Eq (α := α) ((c : (a : α) → α) (⨆ (i : ι), (c : (a : α) → α) (f i)) : α) ((c : (a : α) → α) (⨆ (i : ι), f i) : α)

Tactic:
le_antisymm (le_closure_iff.1 <| iSup_le fun i => c.monotone <| le_iSup f i) <|
    c.monotone <| iSup_mono fun _ => c.le_closure _

Premises used: ClosureOperator.le_closure_iff, le_iSup, ClosureOperator.le_closure, le_antisymm, Iff.mp, iSup_le, ClosureOperator.monotone, iSup_mono
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
c : ClosureOperator α
f : (i : ι) → κ i → α
⊢ Eq (α := α) ((c : (a : α) → α) (⨆ (i : ι), ⨆ (j : κ i), (c : (a : α) → α) (f i j)) : α)
    ((c : (a : α) → α) (⨆ (i : ι), ⨆ (j : κ i), f i j) : α)

Tactic:
le_antisymm (le_closure_iff.1 <| iSup₂_le fun i j => c.monotone <| le_iSup₂ i j) <|
    c.monotone <| iSup₂_mono fun _ _ => c.le_closure _

Premises used: iSup₂_le, iSup₂_mono, ClosureOperator.le_closure_iff, le_iSup₂, ClosureOperator.le_closure, le_antisymm, Iff.mp, ClosureOperator.monotone
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
⊢ GaloisConnection l.toFun u

Tactic:
l.gc'

Premises used: LowerAdjoint.gc'
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
u : β → α
l₁ : α → β
gc' : GaloisConnection l₁ u
l₂ : α → β
gc'_1 : GaloisConnection l₂ u
h : { toFun := l₁, gc' := gc' : LowerAdjoint u }.toFun = { toFun := l₂, gc' := gc'_1 : LowerAdjoint u }.toFun
⊢ { toFun := l₁, gc' := gc' : LowerAdjoint u } = { toFun := l₂, gc' := gc'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
⊢ Monotone (u ∘ l.toFun)

Tactic:
l.gc.monotone_u.comp l.gc.monotone_l

Premises used: GaloisConnection.monotone_u, LowerAdjoint.gc, Monotone.comp, GaloisConnection.monotone_l
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x : α
⊢ x ≤ u (l.toFun x)

Tactic:
l.gc.le_u_l _

Premises used: LowerAdjoint.gc, GaloisConnection.le_u_l
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x : α
⊢ u (l.toFun (u (l.toFun x))) = u (l.toFun x)

Tactic:
l.closureOperator.idempotent _

Premises used: LowerAdjoint.closureOperator, ClosureOperator.idempotent
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
⊢ x ≤ u (l.toFun y) ↔ u (l.toFun x) ≤ u (l.toFun y)

Tactic:
l.closureOperator.le_closure_iff

Premises used: ClosureOperator.le_closure_iff
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x : α
⊢ x ∈ l.closed ↔ u (l.toFun x) = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LowerAdjoint.closed
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x : α
h : x ∈ l.closed
⊢ u (l.toFun x) = x

Tactic:
h

Premises used: Set.Mem, setOf, LowerAdjoint.closed
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x : α
⊢ x ∈ l.closed ↔ u (l.toFun x) ≤ x

Tactic:
l.closureOperator.isClosed_iff_closure_le

Premises used: Set.Mem, setOf, ClosureOperator.isClosed_iff_closure_le, LowerAdjoint.closed
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x : α
⊢ u (l.toFun x) ∈ l.closed

Tactic:
l.idempotent x

Premises used: LowerAdjoint.idempotent, Set.Mem, setOf, LowerAdjoint.closed
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
⊢ l.closed = range (u ∘ l.toFun)

Tactic:
l.closureOperator.setOf_isClosed_eq_range_closure

Premises used: ClosureOperator.setOf_isClosed_eq_range_closure, setOf, LowerAdjoint.closed
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
hy : y ∈ l.closed
⊢ u (l.toFun x) ≤ y ↔ x ≤ y

Tactic:
(show l.closureOperator.IsClosed y from hy).closure_le_iff

Premises used: ClosureOperator.IsClosed.closure_le_iff
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : Preorder β
u : β → α
l : LowerAdjoint u
⊢ u (l.toFun ⊤) = ⊤

Tactic:
l.closureOperator.closure_top

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_top
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SemilatticeInf α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
⊢ u (l.toFun (x ⊓ y)) ≤ u (l.toFun x) ⊓ u (l.toFun y)

Tactic:
l.closureOperator.closure_inf_le x y

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_inf_le
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SemilatticeSup α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
⊢ u (l.toFun x) ⊔ u (l.toFun y) ≤ u (l.toFun (x ⊔ y))

Tactic:
l.closureOperator.closure_sup_closure_le x y

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_sup_closure_le
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SemilatticeSup α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
⊢ u (l.toFun (u (l.toFun x) ⊔ y)) = u (l.toFun (x ⊔ y))

Tactic:
l.closureOperator.closure_sup_closure_left x y

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_sup_closure_left
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SemilatticeSup α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
⊢ u (l.toFun (x ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))

Tactic:
l.closureOperator.closure_sup_closure_right x y

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_sup_closure_right
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SemilatticeSup α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
x y : α
⊢ u (l.toFun (u (l.toFun x) ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))

Tactic:
l.closureOperator.closure_sup_closure x y

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_sup_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_4
inst : CompleteLattice α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
f : ι → α
⊢ u (l.toFun (⨆ (i : ι), u (l.toFun (f i)))) = u (l.toFun (⨆ (i : ι), f i))

Tactic:
l.closureOperator.closure_iSup_closure _

Premises used: LowerAdjoint.closureOperator, ClosureOperator.closure_iSup_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst : CompleteLattice α
inst_1 : Preorder β
u : β → α
l : LowerAdjoint u
f : (i : ι) → κ i → α
⊢ u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), u (l.toFun (f i j)))) = u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), f i j))

Tactic:
l.closureOperator.closure_iSup₂_closure _

Premises used: ClosureOperator.closure_iSup₂_closure, LowerAdjoint.closureOperator
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
⊢ s ⊆ (↑(l.toFun (u := SetLike.coe) s) : Set β)

Tactic:
l.le_closure s

Premises used: LowerAdjoint.le_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
P : β
hP : P ∉ l.toFun (u := SetLike.coe) s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure _ s h)

Premises used: LowerAdjoint.subset_closure, Not
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
S : α
⊢ l.toFun (u := SetLike.coe) s ≤ S ↔ s ⊆ (↑S : Set β)

Tactic:
l.gc s S

Premises used: LowerAdjoint.gc
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
x : β
simp_rw :
  l.toFun (u := SetLike.coe) {x} ≤ l.toFun (u := SetLike.coe) s ↔
    ∀ (S : α), l.toFun (u := SetLike.coe) s ≤ S → l.toFun (u := SetLike.coe) {x} ≤ S
⊢ x ∈ l.toFun (u := SetLike.coe) s ↔ ∀ (S : α), s ⊆ (↑S : Set β) → x ∈ S

Tactic:
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]

Premises used: Set.singleton_subset_iff, LowerAdjoint.le_iff_subset, SetLike.mem_coe
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
x : β
⊢ l.toFun (u := SetLike.coe) {x} ≤ l.toFun (u := SetLike.coe) s ↔
    ∀ (S : α), l.toFun (u := SetLike.coe) s ≤ S → l.toFun (u := SetLike.coe) {x} ≤ S

Tactic:
⟨fun h S => h.trans, fun h => h _ le_rfl⟩

Premises used: le_rfl, Iff.intro, LowerAdjoint.toFun, LE.le.trans
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
x : β
⊢ l.toFun (u := SetLike.coe) {x} ≤ l.toFun (u := SetLike.coe) s ↔
    ∀ (S : α), l.toFun (u := SetLike.coe) s ≤ S → l.toFun (u := SetLike.coe) {x} ≤ S

Tactic:
exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
x y : α
⊢ (↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑(l.toFun (u := SetLike.coe) (↑y : Set β)) : Set β) ⊆
    (↑(l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))) : Set β)

Tactic:
l.closure_sup_closure_le x y

Premises used: SetLike.coe, LowerAdjoint.closure_sup_closure_le
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
x y : α
⊢ l.toFun (u := SetLike.coe) ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑y : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))

Tactic:
SetLike.coe_injective (l.closure_sup_closure_left x y)

Premises used: LowerAdjoint.closure_sup_closure_left, SetLike.coe_injective, SetLike.coe
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
x y : α
⊢ l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑(l.toFun (u := SetLike.coe) (↑y : Set β)) : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))

Tactic:
SetLike.coe_injective (l.closure_sup_closure_right x y)

Premises used: LowerAdjoint.closure_sup_closure_right, SetLike.coe_injective, SetLike.coe
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
x y : α
rw :
  l.toFun (u := SetLike.coe) ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑y : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
rw₁ rw₂ :
  l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β)) = l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))
⊢ l.toFun (u := SetLike.coe)
      ((↑(l.toFun (u := SetLike.coe) (↑x : Set β)) : Set β) ∪ (↑(l.toFun (u := SetLike.coe) (↑y : Set β)) : Set β)) =
    l.toFun (u := SetLike.coe) ((↑x : Set β) ∪ (↑y : Set β))

Tactic:
rw [closure_union_closure_right, closure_union_closure_left]

Premises used: LowerAdjoint.closure_union_closure_right, LowerAdjoint.closure_union_closure_left
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
f : ι → α
⊢ l.toFun (u := SetLike.coe) (⋃ (i : ι), (↑(l.toFun (u := SetLike.coe) (↑(f i) : Set β)) : Set β)) =
    l.toFun (u := SetLike.coe) (⋃ (i : ι), (↑(f i) : Set β))

Tactic:
SetLike.coe_injective <| l.closure_iSup_closure _

Premises used: SetLike.coe_injective, LowerAdjoint.closure_iSup_closure
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst : SetLike α β
inst_1 : Preorder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
f : (i : ι) → κ i → α
⊢ l.toFun (u := SetLike.coe) (⋃ (i : ι), ⋃ (j : κ i), (↑(l.toFun (u := SetLike.coe) (↑(f i j) : Set β)) : Set β)) =
    l.toFun (u := SetLike.coe) (⋃ (i : ι), ⋃ (j : κ i), (↑(f i j) : Set β))

Tactic:
SetLike.coe_injective <| l.closure_iSup₂_closure _

Premises used: LowerAdjoint.closure_iSup₂_closure, SetLike.coe_injective
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
β : Type u_4
inst : SetLike α β
inst_1 : PartialOrder α
l : LowerAdjoint.{u_4, u_1} (β := α) SetLike.coe
s : Set β
S : α
h₁ : s ⊆ (↑S : Set β)
h₂ : S ≤ l.toFun (u := SetLike.coe) s
⊢ l.toFun (u := SetLike.coe) s = S

Tactic:
((l.le_iff_subset _ _).2 h₁).antisymm h₂

Premises used: Iff.mpr, LowerAdjoint.le_iff_subset, LE.le.antisymm
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
a : ∀ (x : α), Eq (α := α) ((⋯.closureOperator : (a : α) → α) x : α) ((c : (a : α) → α) x : α)
⊢ ⋯.closureOperator = c

Tactic:
ext x
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
inst : PartialOrder α
c : ClosureOperator α
x : α
⊢ Eq (α := α) ((⋯.closureOperator : (a : α) → α) x : α) ((c : (a : α) → α) x : α)

Tactic:
rfl
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
inst_1 : IsEmpty α
s : Set α
⊢ IsCofinal s

Tactic:
fun a ↦ isEmptyElim a

Premises used: isEmptyElim, IsCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
⊢ IsCofinal.{u_1} (α := α) ∅ ↔ IsEmpty α

Tactic:
⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩

Premises used: IsEmpty.mk, IsCofinal.of_isEmpty, Iff.intro
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
refine : ∀ (h : IsCofinal.{u_1} (α := α) ∅) (a : α), False
⊢ IsCofinal.{u_1} (α := α) ∅ ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
h : IsCofinal.{u_1} (α := α) ∅
a : α
⊢ False

Tactic:
simpa using h a
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
x : α
⊢ IsCofinal (α := α) {x} ↔ IsTop x

Tactic:
simp [IsCofinal, IsTop]

Premises used: IsTop, IsCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
⊢ IsCofinal (α := α) {⊤}

Tactic:
simp
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a : α
obtain : ∀ (b : α) (hb : b ∈ s) (hb' : a ≤ b), ∃ y ∈ t, a ≤ y
⊢ ∃ y ∈ t, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ t, a ≤ y

Tactic:
⟨b, h hb, hb'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LE α
s t : Set α
h : s ⊆ t
hs : IsCofinal s
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ t, a ≤ y

Tactic:
exact ⟨b, h hb, hb'⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
⊢ IsCofinal.{u_1} (α := α) Set.univ

Tactic:
fun a ↦ ⟨a, ⟨⟩, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro, IsCofinal, True.intro
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
obtain : ∀ (b : α) (hb : a ≤ f b), ∃ y ∈ f '' s, a ≤ y
⊢ ∃ y ∈ f '' s, a ≤ y

Tactic:
obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' a

Premises used: rfl