awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : AddCommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedAddMonoid β
f g : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
hg : IsLocalMinOn g s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x - g x) s a

Tactic:
hf.sub hg

Premises used: IsLocalMaxOn, IsMaxFilter.sub
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
f g : α → β
a : α
hf : IsLocalMin f a
hg : IsLocalMin g a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) a

Tactic:
hf.sup hg

Premises used: IsMinFilter.sup, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
f g : α → β
a : α
hf : IsLocalMax f a
hg : IsLocalMax g a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) a

Tactic:
hf.sup hg

Premises used: IsLocalMax, IsMaxFilter.sup
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
f g : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
hg : IsLocalMinOn g s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) s a

Tactic:
hf.sup hg

Premises used: IsMinFilter.sup, IsLocalMinOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
f g : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
hg : IsLocalMaxOn g s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊔ g x) s a

Tactic:
hf.sup hg

Premises used: IsLocalMaxOn, IsMaxFilter.sup
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
f g : α → β
a : α
hf : IsLocalMin f a
hg : IsLocalMin g a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) a

Tactic:
hf.inf hg

Premises used: IsMinFilter.inf, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
f g : α → β
a : α
hf : IsLocalMax f a
hg : IsLocalMax g a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) a

Tactic:
hf.inf hg

Premises used: IsLocalMax, IsMaxFilter.inf
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
f g : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
hg : IsLocalMinOn g s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) s a

Tactic:
hf.inf hg

Premises used: IsMinFilter.inf, IsLocalMinOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
f g : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
hg : IsLocalMaxOn g s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ f x ⊓ g x) s a

Tactic:
hf.inf hg

Premises used: IsMaxFilter.inf, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : IsLocalMin f a
hg : IsLocalMin g a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) a

Tactic:
hf.min hg

Premises used: IsMinFilter.min, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : IsLocalMax f a
hg : IsLocalMax g a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) a

Tactic:
hf.min hg

Premises used: IsLocalMax, IsMaxFilter.min
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
hg : IsLocalMinOn g s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) s a

Tactic:
hf.min hg

Premises used: IsMinFilter.min, IsLocalMinOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
hg : IsLocalMaxOn g s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ Min.min (f x) (g x)) s a

Tactic:
hf.min hg

Premises used: IsLocalMaxOn, IsMaxFilter.min
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : IsLocalMin f a
hg : IsLocalMin g a
⊢ IsLocalMin.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) a

Tactic:
hf.max hg

Premises used: IsLocalMin, IsMinFilter.max
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
hf : IsLocalMax f a
hg : IsLocalMax g a
⊢ IsLocalMax.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) a

Tactic:
hf.max hg

Premises used: IsLocalMax, IsMaxFilter.max
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsLocalMinOn f s a
hg : IsLocalMinOn g s a
⊢ IsLocalMinOn.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) s a

Tactic:
hf.max hg

Premises used: IsLocalMinOn, IsMinFilter.max
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder β
f g : α → β
a : α
s : Set α
hf : IsLocalMaxOn f s a
hg : IsLocalMaxOn g s a
⊢ IsLocalMaxOn.{u, v} (β := β) (fun (x : α) ↦ Max.max (f x) (g x)) s a

Tactic:
hf.max hg

Premises used: IsLocalMaxOn, IsMaxFilter.max
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
hle : g ≤ᶠ[𝓝[s] a] f
hfga : f a = g a
h : IsLocalMaxOn f s a
⊢ IsLocalMaxOn g s a

Tactic:
hle.isMaxFilter hfga h

Premises used: Filter.EventuallyLE.isMaxFilter, IsLocalMaxOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
h : IsLocalMaxOn f s a
heq : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ IsLocalMaxOn g s a

Tactic:
h.congr heq <| heq.eq_of_nhdsWithin hmem

Premises used: IsMaxFilter.congr, IsLocalMaxOn, Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
heq : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ IsLocalMaxOn f s a ↔ IsLocalMaxOn g s a

Tactic:
heq.isMaxFilter_iff <| heq.eq_of_nhdsWithin hmem

Premises used: IsLocalMaxOn, Filter.EventuallyEq.isMaxFilter_iff, Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
hle : f ≤ᶠ[𝓝[s] a] g
hfga : f a = g a
h : IsLocalMinOn f s a
⊢ IsLocalMinOn g s a

Tactic:
hle.isMinFilter hfga h

Premises used: Filter.EventuallyLE.isMinFilter, IsLocalMinOn
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
h : IsLocalMinOn f s a
heq : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ IsLocalMinOn g s a

Tactic:
h.congr heq <| heq.eq_of_nhdsWithin hmem

Premises used: IsLocalMinOn, IsMinFilter.congr, Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
heq : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ IsLocalMinOn f s a ↔ IsLocalMinOn g s a

Tactic:
heq.isMinFilter_iff <| heq.eq_of_nhdsWithin hmem

Premises used: IsLocalMinOn, Filter.EventuallyEq.eq_of_nhdsWithin, Filter.EventuallyEq.isMinFilter_iff
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
h : IsLocalExtrOn f s a
heq : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ IsLocalExtrOn g s a

Tactic:
h.congr heq <| heq.eq_of_nhdsWithin hmem

Premises used: IsExtrFilter.congr, IsLocalExtrOn, Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
s : Set α
f g : α → β
a : α
heq : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ IsLocalExtrOn f s a ↔ IsLocalExtrOn g s a

Tactic:
heq.isExtrFilter_iff <| heq.eq_of_nhdsWithin hmem

Premises used: IsLocalExtrOn, Filter.EventuallyEq.isExtrFilter_iff, Filter.EventuallyEq.eq_of_nhdsWithin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
hle : g ≤ᶠ[𝓝 a] f
hfga : f a = g a
h : IsLocalMax f a
⊢ IsLocalMax g a

Tactic:
hle.isMaxFilter hfga h

Premises used: IsLocalMax, Filter.EventuallyLE.isMaxFilter
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
h : IsLocalMax f a
heq : f =ᶠ[𝓝 a] g
⊢ IsLocalMax g a

Tactic:
h.congr heq heq.eq_of_nhds

Premises used: IsMaxFilter.congr, IsLocalMax, Filter.EventuallyEq.eq_of_nhds
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
heq : f =ᶠ[𝓝 a] g
⊢ IsLocalMax f a ↔ IsLocalMax g a

Tactic:
heq.isMaxFilter_iff heq.eq_of_nhds

Premises used: IsLocalMax, Filter.EventuallyEq.eq_of_nhds, Filter.EventuallyEq.isMaxFilter_iff
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
hle : f ≤ᶠ[𝓝 a] g
hfga : f a = g a
h : IsLocalMin f a
⊢ IsLocalMin g a

Tactic:
hle.isMinFilter hfga h

Premises used: Filter.EventuallyLE.isMinFilter, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
h : IsLocalMin f a
heq : f =ᶠ[𝓝 a] g
⊢ IsLocalMin g a

Tactic:
h.congr heq heq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, IsMinFilter.congr, IsLocalMin
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
heq : f =ᶠ[𝓝 a] g
⊢ IsLocalMin f a ↔ IsLocalMin g a

Tactic:
heq.isMinFilter_iff heq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, IsLocalMin, Filter.EventuallyEq.isMinFilter_iff
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
h : IsLocalExtr f a
heq : f =ᶠ[𝓝 a] g
⊢ IsLocalExtr g a

Tactic:
h.congr heq heq.eq_of_nhds

Premises used: IsExtrFilter.congr, Filter.EventuallyEq.eq_of_nhds, IsLocalExtr
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder β
f g : α → β
a : α
heq : f =ᶠ[𝓝 a] g
⊢ IsLocalExtr f a ↔ IsLocalExtr g a

Tactic:
heq.isExtrFilter_iff heq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds, IsLocalExtr, Filter.EventuallyEq.isExtrFilter_iff
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
⊢ b ∈ Iic b

Tactic:
simp
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
simp
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
inr : b ≤ x → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
rcases le_total x b

Premises used: le_total
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h_1 : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
aesop
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : MonotoneOn f a
h₁ : AntitoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h_1 : b ≤ x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ f b) x} x

Tactic:
aesop
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
⊢ b ∈ Iic b

Tactic:
simp
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this : b ∈ a
⊢ b ∈ Ici b

Tactic:
simp
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
inl : x ≤ b → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
inr : b ≤ x → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x

Tactic:
rcases le_total x b

Premises used: le_total
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h_1 : x ≤ b
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x

Tactic:
aesop
-- Module: Mathlib.Topology.Order.LocalExtr
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
β : Type u_2
inst_2 : Preorder β
b : α
f : α → β
a : Set α
ha : a ∈ 𝓝[≤] b
c : Set α
hc : c ∈ 𝓝[≥] b
h₀ : AntitoneOn f a
h₁ : MonotoneOn f c
this_1 : b ∈ a
this : b ∈ c
x : α
h : x ∈ a ∩ Iic b ∪ c ∩ Ici b
h_1 : b ≤ x
⊢ Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f b ≤ f x) x} x

Tactic:
aesop
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
⊢ (𝓝[s] x).NeBot

Tactic:
have : (𝓝[s] x).NeBot := hx
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
apply : ∀ (b : α) (hb : b ∈ s) (hbx : b ≤ x), f b ≤ f x
apply₁ : ∀ (b : α) (hb : b ∈ s) (hxb : x ≤ b), f x ≤ f b
⊢ MonotoneOn f (insert x s)

Tactic:
apply monotoneOn_insert_iff.2 ⟨fun b hb hbx ↦ ?_, fun b hb hxb ↦ ?_, hf⟩

Premises used: Iff.mpr, And.intro, Set.monotoneOn_insert_iff
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx : b ≤ x
inl : ∀ (hx : ClusterPt b (𝓟 s)) (h'x : ContinuousWithinAt f s b) (this : (𝓝[s] b).NeBot) (hbx : b ≤ b), f b ≤ f b
inr : ∀ (hbx : b < x), f b ≤ f x
⊢ f b ≤ f x

Tactic:
rcases hbx.eq_or_lt with rfl | hbx

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
b : α
hb : b ∈ s
hx : ClusterPt b (𝓟 s)
h'x : ContinuousWithinAt f s b
this : (𝓝[s] b).NeBot
hbx : b ≤ b
⊢ f b ≤ f b

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
b : α
hb : b ∈ s
hx : ClusterPt b (𝓟 s)
h'x : ContinuousWithinAt f s b
this : (𝓝[s] b).NeBot
hbx : b ≤ b
⊢ f b ≤ f b

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
inr : ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c
⊢ f b ≤ f x

Tactic:
apply ge_of_tendsto h'x

Premises used: ge_of_tendsto
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
⊢ s ∩ Ioi b ∈ 𝓝[s] x

Tactic:
have : s ∩ Ioi b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Ioi_mem_nhds hbx)
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
this : s ∩ Ioi b ∈ 𝓝[s] x
y : α
hy : y ∈ s ∩ Ioi b
⊢ f b ≤ f y

Tactic:
hf hb hy.1 (le_of_lt hy.2)

Premises used: le_of_lt, And.right, And.left
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx_1 : b ≤ x
hbx : b < x
this : s ∩ Ioi b ∈ 𝓝[s] x
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α | x ∈ s ∩ Ioi b → Membership.mem (γ := Set α) {x : α | (fun (c : α) ↦ f b ≤ f c) x} x} a
h₁ h₂ : ∀ (y : α) (hy : y ∈ s ∩ Ioi b), f b ≤ f y
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f b ≤ f c

Tactic:
filter_upwards [this] with y hy using hf hb hy.1 (le_of_lt hy.2)
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
inl : ∀ (hb : x ∈ s) (hxb : x ≤ x), f x ≤ f x
inr : ∀ (hxb : x < b), f x ≤ f b
⊢ f x ≤ f b

Tactic:
rcases hxb.eq_or_lt with rfl | hxb

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
hb : x ∈ s
hxb : x ≤ x
⊢ f x ≤ f x

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
hb : x ∈ s
hxb : x ≤ x
⊢ f x ≤ f x

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
inr : ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b
⊢ f x ≤ f b

Tactic:
apply le_of_tendsto h'x

Premises used: le_of_tendsto
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
⊢ s ∩ Iio b ∈ 𝓝[s] x

Tactic:
have : s ∩ Iio b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Iio_mem_nhds hxb)
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
this : s ∩ Iio b ∈ 𝓝[s] x
h : ∀ (y : α) (hy : y ∈ s ∩ Iio b), f y ≤ f b
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
this : s ∩ Iio b ∈ 𝓝[s] x
y : α
hy : y ∈ s ∩ Iio b
⊢ f y ≤ f b

Tactic:
hf hy.1 hb (le_of_lt hy.2)

Premises used: le_of_lt, And.right, And.left
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
x : α
f : α → β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this_1 : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb_1 : x ≤ b
hxb : x < b
this : s ∩ Iio b ∈ 𝓝[s] x
y : α
hy : y ∈ s ∩ Iio b
⊢ f y ≤ f b

Tactic:
exact hf hy.1 hb (le_of_lt hy.2)

Premises used: le_of_lt, And.right, And.left
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
s : Set α
f : α → β
inst_4 : SecondCountableTopology α
hf : MonotoneOn f s
⊢ Nontrivial α

Tactic:
nontriviality α