awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIciTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), a < f i
hlim : Tendsto f F (𝓝 a)
⊢ ⋃ (i : ι), Ici (f i) = Ioi a

Tactic:
iUnion_Iic_eq_Iio_of_lt_of_tendsto (α := αᵒᵈ) hlt hlim

Premises used: Set.Ioi, Set.Ici, iUnion_Iic_eq_Iio_of_lt_of_tendsto, setOf, OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
p : α → Prop
⊢ OrderClosedTopology.{u} (Subtype p)

Tactic:
have this : Continuous fun p : Subtype p × Subtype p => ((p.fst : α), (p.snd : α)) :=
    continuous_subtype_val.prodMap continuous_subtype_val
  OrderClosedTopology.mk (t.isClosed_le'.preimage this)

Premises used: continuous_subtype_val, Continuous.prodMap, OrderClosedTopology.isClosed_le', OrderClosedTopology.mk, IsClosed.preimage
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
⊢ IsClosed[instTopologicalSpaceProd] {p : α × α | p.1 ≤ p.2}

Tactic:
t.isClosed_le'

Premises used: OrderClosedTopology.isClosed_le'
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
⊢ IsClosed[instTopologicalSpaceProd] {p : α × α | p.2 ≤ p.1}

Tactic:
(isClosed_le_prod (α := α)).preimage continuous_swap

Premises used: Set.Mem, setOf, continuous_swap, Set.preimage, IsClosed.preimage, isClosed_le_prod
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_2, inst] f
hg : Continuous[inst_2, inst] g
⊢ IsClosed[inst_2] {b : β | f b ≤ g b}

Tactic:
continuous_iff_isClosed.mp (hf.prodMk hg) _ isClosed_le_prod

Premises used: Set.Mem, setOf, continuous_iff_isClosed, Set.preimage, Iff.mp, isClosed_le_prod, Continuous.prodMk
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
⊢ OrderClosedTopology.{u} αᵒᵈ

Tactic:
⟨isClosed_le_prod' (α := α)⟩

Premises used: OrderClosedTopology.mk, isClosed_le_prod'
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
a b : α
⊢ IsClosed[inst] (Icc a b)

Tactic:
IsClosed.inter isClosed_Ici isClosed_Iic

Premises used: Set.Mem, setOf, Set.inter, isClosed_Iic, Set.Icc, IsClosed.inter, isClosed_Ici
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
a b : α
⊢ closure[inst] (Icc a b) = Icc a b

Tactic:
isClosed_Icc.closure_eq

Premises used: IsClosed.closure_eq, isClosed_Icc
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
f g : β → α
b : Filter β
a₁ a₂ : α
hf : Tendsto f b (𝓝 a₁)
hg : Tendsto g b (𝓝 a₂)
h : ∃ᶠ (x : β) in b, f x ≤ g x
⊢ a₁ ≤ a₂

Tactic:
t.isClosed_le'.mem_of_frequently_of_tendsto h (hf.prodMk_nhds hg)

Premises used: Set.Mem, setOf, OrderClosedTopology.isClosed_le', IsClosed.mem_of_frequently_of_tendsto, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
f g : β → α
b : Filter β
a₁ a₂ : α
inst_2 : b.NeBot
hf : Tendsto f b (𝓝 a₁)
hg : Tendsto g b (𝓝 a₂)
h : f ≤ᶠ[b] g
⊢ a₁ ≤ a₂

Tactic:
le_of_tendsto_of_tendsto_of_frequently hf hg <| Eventually.frequently h

Premises used: le_of_tendsto_of_tendsto_of_frequently, Filter.Eventually.frequently
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
f g : β → α
b : Filter β
a₁ a₂ : α
inst_2 : b.NeBot
hf : Tendsto f b (𝓝 a₁)
hg : Tendsto g b (𝓝 a₂)
h : ∀ (x : β), f x ≤ g x
⊢ a₁ ≤ a₂

Tactic:
le_of_tendsto_of_tendsto hf hg (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, le_of_tendsto_of_tendsto
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_2, inst] f
hg : Continuous[inst_2, inst] g
⊢ Eq.{v + 1} (α := Set β) (closure[inst_2] {b : β | f b ≤ g b}) {b : β | f b ≤ g b}

Tactic:
(isClosed_le hf hg).closure_eq

Premises used: IsClosed.closure_eq, isClosed_le
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_2, inst] f
hg : Continuous[inst_2, inst] g
⊢ Subset.{v} (α := Set β) (closure[inst_2] {b : β | f b < g b}) {b : β | f b ≤ g b}

Tactic:
(closure_minimal fun _ => le_of_lt) <| isClosed_le hf hg

Premises used: closure_minimal, setOf, le_of_lt, isClosed_le
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f g : β → α
s : Set β
x : β
hx : x ∈ closure[inst_2] s
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
h : ∀ y ∈ s, f y ≤ g y
⊢ f x ≤ g x

Tactic:
show (f x, g x) ∈ { p : α × α | p.1 ≤ p.2 } from
    OrderClosedTopology.isClosed_le'.closure_subset ((hf.prodMk hg).mem_closure hx h)

Premises used: ContinuousWithinAt.mem_closure, Set.Mem, setOf, OrderClosedTopology.isClosed_le', IsClosed.closure_subset, ContinuousWithinAt.prodMk
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f g : β → α
s : Set β
hs : IsClosed[inst_2] s
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ IsClosed[inst_2] {x : β | x ∈ s ∧ f x ≤ g x}

Tactic:
(hf.prodMk hg).preimage_isClosed_of_isClosed hs OrderClosedTopology.isClosed_le'

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, Set.Mem, setOf, OrderClosedTopology.isClosed_le', Set.inter, Set.preimage, ContinuousOn.prodMk
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f g : β → α
s : Set β
h : ∀ x ∈ s, f x ≤ g x
hf : ContinuousOn f (closure[inst_2] s)
hg : ContinuousOn g (closure[inst_2] s)
x : β
hx : x ∈ closure[inst_2] s
⊢ f x ≤ g x

Tactic:
have : s ⊆ { y ∈ closure s | f y ≤ g y } := fun y hy => ⟨subset_closure hy, h y hy⟩
  (closure_minimal this (isClosed_closure.isClosed_le hf hg) hx).2

Premises used: subset_closure, closure_minimal, And.right, And.intro, IsClosed.isClosed_le, isClosed_closure
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : TopologicalSpace β
f : β → α
s : Set β
hs : IsClosed[inst_2] s
hf : ContinuousOn f s
⊢ IsClosed[instTopologicalSpaceProd] {p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
(hs.preimage continuous_fst).isClosed_le (hf.comp continuousOn_fst Subset.rfl) continuousOn_snd

Premises used: Set.Mem, setOf, continuous_fst, ContinuousOn.comp, continuousOn_snd, continuousOn_fst, Set.Subset.rfl, Set.preimage, IsClosed.isClosed_le, IsClosed.preimage
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
simp :
  ∀ (a : β → α),
    (∃ᶠ (y : β → α) in 𝓝 a, Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} y) →
      Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} a
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | MonotoneOn f s}

Tactic:
simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]

Premises used: isClosed_iff_clusterPt, clusterPt_principal_iff_frequently
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
g : β → α
hg : ∃ᶠ (y : β → α) in 𝓝 g, Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} y
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
⊢ ∀ (x : β), Tendsto (fun (f' : β → α) ↦ f' x) (𝓝 g) (𝓝 (g x))

Tactic:
have hmain (x) : Tendsto (fun f' ↦ f' x) (𝓝 g) (𝓝 (g x)) := continuousAt_apply x _
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
g : β → α
hg : ∃ᶠ (y : β → α) in 𝓝 g, Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} y
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
hmain : ∀ (x : β), Tendsto (fun (f' : β → α) ↦ f' x) (𝓝 g) (𝓝 (g x))
⊢ g a ≤ g b

Tactic:
le_of_tendsto_of_tendsto_of_frequently (hmain a) (hmain b) (hg.mono fun g h ↦ h ha hb hab)

Premises used: le_of_tendsto_of_tendsto_of_frequently, Filter.Frequently.mono
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
g : β → α
hg : ∃ᶠ (y : β → α) in 𝓝 g, Membership.mem (γ := Set (β → α)) {f : β → α | MonotoneOn f s} y
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hab : a ≤ b
hmain : ∀ (x : β), Tendsto (fun (f' : β → α) ↦ f' x) (𝓝 g) (𝓝 (g x))
⊢ g a ≤ g b

Tactic:
exact le_of_tendsto_of_tendsto_of_frequently (hmain a) (hmain b) (hg.mono fun g h ↦ h ha hb hab)

Premises used: le_of_tendsto_of_tendsto_of_frequently, Filter.Frequently.mono
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
simp_rw : IsClosed[Pi.topologicalSpace] {f : β → α | MonotoneOn f univ}
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | Monotone f}

Tactic:
simp_rw [← monotoneOn_univ]

Premises used: monotoneOn_univ
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | MonotoneOn f univ}

Tactic:
isClosed_monotoneOn

Premises used: isClosed_monotoneOn
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | MonotoneOn f univ}

Tactic:
exact isClosed_monotoneOn

Premises used: isClosed_monotoneOn
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
s : Set β
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | AntitoneOn f s}

Tactic:
isClosed_monotoneOn (α := αᵒᵈ) (β := β)

Premises used: setOf, AntitoneOn, OrderDual, isClosed_monotoneOn
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
t : OrderClosedTopology α
inst_2 : Preorder β
⊢ IsClosed[Pi.topologicalSpace] {f : β → α | Antitone f}

Tactic:
isClosed_monotone (α := αᵒᵈ) (β := β)

Premises used: setOf, Antitone, isClosed_monotone, OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : PartialOrder α
t : OrderClosedTopology α
⊢ IsClosed[instTopologicalSpaceProd] (diagonal α)

Tactic:
simpa only [diagonal, le_antisymm_iff] using
      t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst)

Premises used: isClosed_le, OrderClosedTopology.isClosed_le', continuous_snd, continuous_fst, Set.diagonal, le_antisymm_iff, IsClosed.inter
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : TopologicalSpace β
f g : β → α
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
⊢ IsOpen[inst_3] {b : β | f b < g b}

Tactic:
simpa only [lt_iff_not_ge] using (isClosed_le hg hf).isOpen_compl

Premises used: lt_iff_not_ge, IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
⊢ IsOpen[instTopologicalSpaceProd] {p : α × α | p.1 < p.2}

Tactic:
isOpen_lt continuous_fst continuous_snd

Premises used: isOpen_lt, continuous_snd, continuous_fst
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a b : α
⊢ IsOpen[inst] (Ioo a b)

Tactic:
IsOpen.inter isOpen_Ioi isOpen_Iio

Premises used: Set.Mem, setOf, isOpen_Iio, Set.inter, isOpen_Ioi, IsOpen.inter, Set.Ioo
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a b : α
⊢ interior (Ioo a b) = Ioo a b

Tactic:
isOpen_Ioo.interior_eq

Premises used: isOpen_Ioo, IsOpen.interior_eq
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a b : α
⊢ Ioo a b ⊆ closure[inst] (interior (Ioo a b))

Tactic:
simp only [interior_Ioo, subset_closure]

Premises used: subset_closure, interior_Ioo
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a b x : α
ha : a < x
hb : x < b
⊢ Ioo a b ∈ 𝓝 x

Tactic:
IsOpen.mem_nhds isOpen_Ioo ⟨ha, hb⟩

Premises used: isOpen_Ioo, And.intro, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a b x : α
ha : a < x
hb : x < b
⊢ Ioc a b ∈ 𝓝 x

Tactic:
mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Ioc_self

Premises used: Ioo_mem_nhds, Set.Ioo_subset_Ioc_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a b x : α
ha : a < x
hb : x < b
⊢ Icc a b ∈ 𝓝 x

Tactic:
mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, Ioo_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
⊢ DiscreteTopology α

Tactic:
discreteTopology_iff_nhds.mpr fun a ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
refine : ∀ (a : α), 𝓝 a = pure a
⊢ DiscreteTopology α

Tactic:
refine discreteTopology_iff_nhds.mpr fun a ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
inst_3 : PredOrder α
inst_4 : SuccOrder α
a : α
rw : 𝓝[univ] a = pure a
rw₁ : 𝓝[Iic a ∪ Ioi a] a = pure a
rw₂ : α
rw₃ : 𝓝[≤] a ⊔ 𝓝[>] a = pure a
rw₄ : α
rw₅ : pure a ⊔ 𝓝[>] a = pure a
rw₆ : Eq (α := Filter α) (pure a ⊔ ⊥) (pure a)
rw₇ rw₈ : Eq (α := Filter α) (pure a) (pure a)
⊢ 𝓝 a = pure a

Tactic:
rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
    sup_bot_eq]

Premises used: nhdsWithin_univ, sup_bot_eq, Set.Iic_union_Ioi, SuccOrder.nhdsGT, nhdsWithin_union, PredOrder.nhdsLE
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
⊢ Subset.{v} (α := Set β) {b : β | f b < g b} (interior {b : β | f b ≤ g b})

Tactic:
(interior_maximal fun _ => le_of_lt) <| isOpen_lt hf hg

Premises used: isOpen_lt, setOf, le_of_lt, interior_maximal
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
rw : Subset.{v} (α := Set β) ({b : β | f b ≤ g b} ∩ closure[inst_3] {b : β | f b ≤ g b}ᶜ) {b : β | f b = g b}
⊢ Subset.{v} (α := Set β) (frontier {b : β | f b ≤ g b}) {b : β | f b = g b}

Tactic:
rw [frontier_eq_closure_inter_closure, closure_le_eq hf hg]

Premises used: closure_le_eq, frontier_eq_closure_inter_closure
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
⊢ Membership.mem (γ := Set β) {b : β | f b = g b} b

Tactic:
le_antisymm hb₁ (closure_lt_subset_le hg hf ?_)

Premises used: closure_lt_subset_le, Set.Mem, setOf, le_antisymm
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
refine : Membership.mem (γ := Set β) (closure[inst_3] {b : β | g b < f b}) b
⊢ Membership.mem (γ := Set β) {b : β | f b = g b} b

Tactic:
refine le_antisymm hb₁ (closure_lt_subset_le hg hf ?_)

Premises used: closure_lt_subset_le, le_antisymm
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
⊢ Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b

Tactic:
hb₂
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
h : Eq.{v + 1} (α := Set β) {b : β | g b < f b} {b : β | f b ≤ g b}ᶜ
⊢ Membership.mem (γ := Set β) (closure[inst_3] {b : β | g b < f b}) b

Tactic:
convert! hb₂ using 2
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
h : Eq.{v + 1} (α := Set β) {b : β | ¬f b ≤ g b} {b : β | f b ≤ g b}ᶜ
⊢ Eq.{v + 1} (α := Set β) {b : β | g b < f b} {b : β | f b ≤ g b}ᶜ

Tactic:
simp only [not_le.symm]

Premises used: not_le, Iff.symm
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
b : β
hb₁ : Membership.mem (γ := Set β) {b : β | f b ≤ g b} b
hb₂ : Membership.mem (γ := Set β) (closure[inst_3] {b : β | f b ≤ g b}ᶜ) b
⊢ Eq.{v + 1} (α := Set β) {b : β | ¬f b ≤ g b} {b : β | f b ≤ g b}ᶜ

Tactic:
rfl
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
a : α
⊢ frontier (Iic a) ⊆ {a}

Tactic:
frontier_le_subset_eq (@continuous_id α _) continuous_const

Premises used: continuous_const, setOf, continuous_id, Set.singleton, frontier_le_subset_eq, Set.Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
⊢ Subset.{v} (α := Set β) (frontier {b : β | f b < g b}) {b : β | f b = g b}

Tactic:
simpa only [← not_lt, ← compl_setOf, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf

Premises used: frontier_compl, eq_comm, not_lt, frontier_le_subset_eq, Set.compl_setOf
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hf' : ContinuousOn f' {x : β | f x ≤ g x}
hg' : ContinuousOn g' {x : β | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
⊢ Continuous[inst_3, inst_4] fun (x : β) ↦ if f x ≤ g x then f' x else g' x

Tactic:
continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)

Premises used: continuous_if, frontier_le_subset_eq, ContinuousOn.mono
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hf' : ContinuousOn f' {x : β | f x ≤ g x}
hg' : ContinuousOn g' {x : β | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
refine_1 : ContinuousOn f' (closure[inst_3] {x : β | f x ≤ g x})
refine_2 : Subset.{v} (α := Set β) (closure[inst_3] {x : β | ¬f x ≤ g x}) {x : β | g x ≤ f x}
⊢ Continuous[inst_3, inst_4] fun (x : β) ↦ if f x ≤ g x then f' x else g' x

Tactic:
refine continuous_if (fun a ha => hfg _ (frontier_le_subset_eq hf hg ha)) ?_ (hg'.mono ?_)

Premises used: continuous_if, frontier_le_subset_eq, ContinuousOn.mono
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hf' : ContinuousOn f' {x : β | f x ≤ g x}
hg' : ContinuousOn g' {x : β | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
refine_1 refine_1₁ refine_1₂ refine_1₃ : ContinuousOn f' {b : β | f b ≤ g b}
⊢ ContinuousOn f' (closure[inst_3] {x : β | f x ≤ g x})

Tactic:
rwa [(isClosed_le hf hg).closure_eq]

Premises used: IsClosed.closure_eq, isClosed_le
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderClosedTopology α
f g : β → α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
inst_5 : (x : β) → Decidable (f x ≤ g x)
f' g' : β → γ
hf : Continuous[inst_3, inst] f
hg : Continuous[inst_3, inst] g
hf' : ContinuousOn f' {x : β | f x ≤ g x}
hg' : ContinuousOn g' {x : β | g x ≤ f x}
hfg : ∀ (x : β), f x = g x → f' x = g' x
refine_2 : Subset.{v} (α := Set β) (closure[inst_3] {x : β | g x < f x}) {x : β | g x ≤ f x}
⊢ Subset.{v} (α := Set β) (closure[inst_3] {x : β | ¬f x ≤ g x}) {x : β | g x ≤ f x}

Tactic:
simp only [not_le]

Premises used: not_le