awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
rcases :
  ∀ (t : Set α) (hts : t ⊆ s) (htc : t.Countable) (htd : Dense t),
    ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t

Tactic:
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩

Premises used: Dense.exists_countable_dense_subset
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t

Tactic:
⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩

Premises used: setOf, IsBot, SDiff.sdiff, And.intro, Exists.intro, IsTop, Union.union
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s
refine_2 : (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable
refine_3 : Dense (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}))
refine_4 : ∀ (x : α) (hx : IsBot x), x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})
refine_5 : ∀ (x : α) (hx : IsTop x), x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t

Tactic:
refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s

Tactic:
diff_subset.trans hts

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s

Tactic:
exact diff_subset.trans hts

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable

Tactic:
htc.mono diff_subset

Premises used: Set.diff_subset, Set.Countable.mono
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable

Tactic:
exact htc.mono diff_subset

Premises used: Set.diff_subset, Set.Countable.mono
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}))

Tactic:
htd.diff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite)

Premises used: Set.Finite.union, Set.subsingleton_isTop, Dense.diff_finite, Set.subsingleton_isBot, Set.Subsingleton.finite
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}))

Tactic:
exact htd.diff_finite ((subsingleton_isBot α).finite.union (subsingleton_isTop α).finite)

Premises used: Set.Finite.union, Set.subsingleton_isTop, Dense.diff_finite, Set.subsingleton_isBot, Set.Subsingleton.finite
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsBot x
⊢ x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
x : α
hx : IsTop x
⊢ x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
inst_5 : Nontrivial α
⊢ ∃ (s : Set α), s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s

Tactic:
simpa using dense_univ.exists_countable_dense_subset_no_bot_top

Premises used: dense_univ, Dense.exists_countable_dense_subset_no_bot_top
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed[inst] (Ico a b)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
refine : ∀ (h : IsClosed[inst] (Ico a b)) (hab : a < b), False
⊢ IsClosed[inst] (Ico a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ico a b)
hab : a < b
⊢ closure[inst] (Ico a b) = Ico a b

Tactic:
have := h.closure_eq
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ico a b)
hab : a < b
this : closure[inst] (Ico a b) = Ico a b
⊢ ¬a ≤ b

Tactic:
rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this

Premises used: Set.Icc_eq_Ico_same_iff, closure_Ico, LT.lt.ne
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ico a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
this hab.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ico a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed[inst] (Ioc a b)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
refine : ∀ (h : IsClosed[inst] (Ioc a b)) (hab : a < b), False
⊢ IsClosed[inst] (Ioc a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioc a b)
hab : a < b
⊢ closure[inst] (Ioc a b) = Ioc a b

Tactic:
have := h.closure_eq
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioc a b)
hab : a < b
this : closure[inst] (Ioc a b) = Ioc a b
⊢ ¬a ≤ b

Tactic:
rw [closure_Ioc hab.ne, Icc_eq_Ioc_same_iff] at this

Premises used: Set.Icc_eq_Ioc_same_iff, LT.lt.ne, closure_Ioc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
this hab.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ b ≤ a → IsClosed[inst] (Ioo a b)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
refine : ∀ (h : IsClosed[inst] (Ioo a b)) (hab : a < b), False
⊢ IsClosed[inst] (Ioo a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioo a b)
hab : a < b
⊢ closure[inst] (Ioo a b) = Ioo a b

Tactic:
have := h.closure_eq
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioo a b)
hab : a < b
this : closure[inst] (Ioo a b) = Ioo a b
⊢ ¬a ≤ b

Tactic:
rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this

Premises used: Set.Icc_eq_Ioo_same_iff, LT.lt.ne, closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
this hab.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : IsClosed[inst] (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
exact this hab.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
⊢ IsMaxOn f (closure[inst] s) a

Tactic:
fun x hx =>
  ContinuousWithinAt.closure_le hx ((hc x hx).mono subset_closure) continuousWithinAt_const h

Premises used: Set.Mem, subset_closure, IsMaxOn, Filter.Eventually, setOf, Set.Subset, ContinuousWithinAt.mono, ContinuousWithinAt.closure_le, continuousWithinAt_const, IsMaxFilter
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsMinOn f s a
hc : ContinuousOn f (closure[inst] s)
⊢ IsMinOn f (closure[inst] s) a

Tactic:
h.dual.closure hc

Premises used: IsMinFilter, IsMinOn, IsMaxOn.closure, IsMinOn.dual
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsExtrOn f s a
hc : ContinuousOn f (closure[inst] s)
⊢ IsExtrOn f (closure[inst] s) a

Tactic:
h.elim (fun h => Or.inl <| h.closure hc) fun h => Or.inr <| h.closure hc

Premises used: IsMaxOn.closure, IsMinOn.closure, IsExtrOn.elim, Or.inl, Or.inr
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
rcases :
  ∀ (U : Set X) (Uo : IsOpen[inst] U) (aU : a ∈ U) (hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}),
    IsLocalMaxOn f (closure[inst] s) a
⊢ IsLocalMaxOn f (closure[inst] s) a

Tactic:
rcases mem_nhdsWithin.1 h with ⟨U, Uo, aU, hU⟩

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
⊢ IsLocalMaxOn f (closure[inst] s) a

Tactic:
mem_nhdsWithin.2 ⟨U, Uo, aU, ?_⟩

Premises used: Iff.mpr, Filter.Eventually, IsLocalMaxOn, mem_nhdsWithin, And.intro, Exists.intro, IsMaxFilter
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
refine : U ∩ closure[inst] s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
⊢ IsLocalMaxOn f (closure[inst] s) a

Tactic:
refine mem_nhdsWithin.2 ⟨U, Uo, aU, ?_⟩

Premises used: Iff.mpr, mem_nhdsWithin, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x ≤ f a) x} x

Tactic:
ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU

Premises used: Set.Mem, setOf, ContinuousWithinAt.closure_le, continuousWithinAt_const
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
refine_1 : x ∈ closure[inst] (U ∩ s)
refine_2 : ContinuousWithinAt f (U ∩ s) x
⊢ Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x ≤ f a) x} x

Tactic:
refine ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU

Premises used: ContinuousWithinAt.closure_le, continuousWithinAt_const
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
refine_1 : U ∈ 𝓝[s] x
⊢ x ∈ closure[inst] (U ∩ s)

Tactic:
rwa [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_inter_of_mem, ←
      mem_closure_iff_nhdsWithin_neBot]

Premises used: nhdsWithin_inter_of_mem, mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ U ∈ 𝓝[s] x

Tactic:
nhdsWithin_le_nhds (Uo.mem_nhds hxU)

Premises used: nhdsWithin_le_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ U ∈ 𝓝[s] x

Tactic:
exact nhdsWithin_le_nhds (Uo.mem_nhds hxU)

Premises used: nhdsWithin_le_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ ContinuousWithinAt f (U ∩ s) x

Tactic:
(hc _ hxs).mono (inter_subset_right.trans subset_closure)

Premises used: subset_closure, HasSubset.Subset.trans, ContinuousWithinAt.mono, Set.inter_subset_right
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMaxOn f s a
hc : ContinuousOn f (closure[inst] s)
U : Set X
Uo : IsOpen[inst] U
aU : a ∈ U
hU : U ∩ s ⊆ {x : X | (fun (x : X) ↦ f x ≤ f a) x}
x : X
hxU : x ∈ U
hxs : x ∈ closure[inst] s
⊢ ContinuousWithinAt f (U ∩ s) x

Tactic:
exact (hc _ hxs).mono (inter_subset_right.trans subset_closure)

Premises used: subset_closure, HasSubset.Subset.trans, ContinuousWithinAt.mono, Set.inter_subset_right
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalMinOn f s a
hc : ContinuousOn f (closure[inst] s)
⊢ IsLocalMinOn f (closure[inst] s) a

Tactic:
IsLocalMaxOn.closure h.dual hc

Premises used: IsMinFilter.dual, IsLocalMinOn, IsMinFilter, IsLocalMaxOn.closure
-- Module: Mathlib.Topology.Order.ExtrClosure
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : Preorder Y
inst_3 : OrderClosedTopology Y
f : X → Y
s : Set X
a : X
h : IsLocalExtrOn f s a
hc : ContinuousOn f (closure[inst] s)
⊢ IsLocalExtrOn f (closure[inst] s) a

Tactic:
h.elim (fun h => Or.inl <| h.closure hc) fun h => Or.inr <| h.closure hc

Premises used: IsLocalMinOn.closure, Or.inl, IsLocalExtrOn.elim, IsLocalMaxOn.closure, Or.inr
-- Module: Mathlib.Topology.Order.Filter
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PartialOrder X
inst_2 : OrderTopology X
inst_3 : NoMaxOrder X
⊢ Tendsto.{u_2, u_2} (α := X) 𝓝 atTop (𝓝 atTop)

Tactic:
Filter.tendsto_nhds_atTop_iff.2 fun x => (eventually_gt_atTop x).mono fun _ => le_mem_nhds

Premises used: Iff.mpr, Filter.Eventually.mono, le_mem_nhds, Filter.tendsto_nhds_atTop_iff, Filter.eventually_gt_atTop
-- Module: Mathlib.Topology.Order.Filter
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : PartialOrder X
inst_2 : OrderTopology X
inst_3 : NoMinOrder X
⊢ Tendsto.{u_2, u_2} (α := X) 𝓝 atBot (𝓝 atBot)

Tactic:
@Filter.tendsto_nhds_atTop Xᵒᵈ _ _ _ _

Premises used: setOf, Filter.atBot, Set.Iic, Filter.tendsto_nhds_atTop, OrderDual
-- Module: Mathlib.Topology.Order.Filter
Goal:
α : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : PartialOrder X
inst_2 : OrderTopology X
inst_3 : NoMaxOrder X
f : α → X
l : Filter α
h : Tendsto f l atTop
⊢ Tendsto (𝓝 ∘ f) l (𝓝 atTop)

Tactic:
Filter.tendsto_nhds_atTop.comp h

Premises used: Filter.tendsto_nhds_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Order.Filter
Goal:
α : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : PartialOrder X
inst_2 : OrderTopology X
inst_3 : NoMinOrder X
f : α → X
l : Filter α
h : Tendsto f l atBot
⊢ Tendsto (𝓝 ∘ f) l (𝓝 atBot)

Tactic:
@Tendsto.nhds_atTop α Xᵒᵈ _ _ _ _ _ _ h

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.Tendsto.nhds_atTop
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : FunLike F α β
inst_5 : ContinuousOrderHomClass F α β
⊢ OrderHomClass F α β

Tactic:
{ ‹ContinuousOrderHomClass F α β› with
    map_rel := ContinuousOrderHomClass.map_monotone }

Premises used: RelHomClass.mk, ContinuousOrderHomClass.map_monotone
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
f g : α →Co β
h : Eq (α := (a : α) → β) ((fun (f : α →Co β) ↦ f.toFun) f) ((fun (f : α →Co β) ↦ f.toFun) g)
obtain :
  ∀ (toFun : α → β) (monotone' : Monotone toFun)
    (continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →Co β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun })
        ((fun (f : α →Co β) ↦ f.toFun) g)),
    { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β } = g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.Order.Hom.Basic
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : TopologicalSpace β
inst_3 : Preorder β
inst_4 : TopologicalSpace γ
inst_5 : Preorder γ
inst_6 : TopologicalSpace δ
inst_7 : Preorder δ
g : α →Co β
toFun : α → β
monotone' : Monotone toFun
continuous_toFun : Continuous { toFun := toFun, monotone' := monotone' : α →o β }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →Co β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun })
    ((fun (f : α →Co β) ↦ f.toFun) g)
obtain :
  ∀ (toFun_1 : α → β) (monotone'_1 : Monotone toFun_1)
    (continuous_toFun_1 : Continuous { toFun := toFun_1, monotone' := monotone'_1 : α →o β }.toFun)
    (h :
      Eq (α := (a : α) → β)
        ((fun (f : α →Co β) ↦ f.toFun) { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun })
        ((fun (f : α →Co β) ↦ f.toFun)
          { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 })),
    { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β } =
      { toFun := toFun_1, monotone' := monotone'_1, continuous_toFun := continuous_toFun_1 }
⊢ { toFun := toFun, monotone' := monotone', continuous_toFun := continuous_toFun : α →Co β } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g