awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c ≤ b
hac₁ : a < c
⊢ f c ≤ b

Tactic:
rw [h_mono.lt_iff_lt has hcs] at hac

Premises used: StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
h : ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
filter_upwards [hs, Ico_mem_nhdsGE hac]

Premises used: Ico_mem_nhdsGE
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
x : α
hx : x ∈ s
left : a ≤ x
hxc : x < c
⊢ f x < b

Tactic:
((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb

Premises used: Iff.mpr, LT.lt.trans_le, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
x : α
hx : x ∈ s
left : a ≤ x
hxc : x < c
⊢ f x < b

Tactic:
exact ((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb

Premises used: Iff.mpr, LT.lt.trans_le, StrictMonoOn.lt_iff_lt
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ a ∈ s

Tactic:
have has : a ∈ s := mem_of_mem_nhdsWithin self_mem_Ici hs
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩

Premises used: Iff.mpr, ContinuousWithinAt, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
refine_1 : ∀ (b : β) (hb : b < f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
refine_2 : ∀ (b : β) (hb : b > f a), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
refine tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b < f a
a_1 : α
hxs : a_1 ∈ s
hxa : a_1 ∈ Ici a
⊢ b < f a_1

Tactic:
hb.trans_le
      (h_mono has hxs hxa)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b < f a
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        x ∈ s →
          Membership.mem (γ := Set α)
            {x : α | x ∈ Ici a → Membership.mem (γ := Set α) {x : α | (fun (b_1 : α) ↦ b < f b_1) x} x} x}
      a_1
h₁ h₂ : ∀ (a_1 : α) (hxs : a_1 ∈ s) (hxa : a_1 ∈ Ici a), b < f a_1
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1

Tactic:
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
refine_2 : ∀ (c : α) (hcs : c ∈ s) (hac : f a < f c) (hcb : f c < b), ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
⊢ a < c

Tactic:
have : a < c := not_le.1 fun h => hac.not_ge <| h_mono hcs has h
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
h : ∀ a_1 ∈ s, a_1 ∈ Ico a c → f a_1 < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
filter_upwards [hs, Ico_mem_nhdsGE this]

Premises used: Ico_mem_nhdsGE
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
x : α
hx : x ∈ s
left : a ≤ x
hxc : x < c
⊢ f x < b

Tactic:
(h_mono hx hcs hxc.le).trans_lt hcb

Premises used: LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
x : α
hx : x ∈ s
left : a ≤ x
hxc : x < c
⊢ f x < b

Tactic:
exact (h_mono hx hcs hxc.le).trans_lt hcb

Premises used: LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_

Premises used: continuousWithinAt_right_of_monotoneOn_of_exists_between
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
refine : ∀ (b : β) (hb : b > f a), ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
refine continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => ?_

Premises used: continuousWithinAt_right_of_monotoneOn_of_exists_between
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
rcases :
  ∀ (b' : β) (hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)) (hab' : f a < b') (hbb' : b' ≤ b),
    ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩

Premises used: mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset, Iff.mp
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
rcases : ∀ (c' : β) (hc' : f a < c' ∧ c' < b'), ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
rcases exists_between hab' with ⟨c', hc'⟩

Premises used: exists_between
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
rcases : ∀ (c : α) (hcs : c ∈ s) (hc : f c ∈ Ioo (f a) b'), ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with
    ⟨_, hc, ⟨c, hcs, rfl⟩⟩

Premises used: mem_closure_iff, isOpen_Ioo, LT.lt.le, And.right, And.left, And.intro, Iff.mp, Set.Ioo, rfl
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩

Premises used: And.right, And.left, LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure[inst_4] (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c ∈ s, f c ∈ Ioo (f a) b

Tactic:
exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : f '' s ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs <|
    mem_of_superset hfs subset_closure

Premises used: subset_closure, continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin
    (fun _ hx _ hy => (h_mono.le_iff_le hx hy).2) hs hfs

Premises used: Iff.mpr, continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin, StrictMonoOn.le_iff_le
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : f '' s ∈ 𝓝[≥] f a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
h_mono.continuousWithinAt_right_of_closure_image_mem_nhdsWithin hs
    (mem_of_superset hfs subset_closure)

Premises used: StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin, subset_closure, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : SurjOn f s (Ioi (f a))
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
h_mono.continuousWithinAt_right_of_exists_between hs fun _ hb =>
    let ⟨c, hcs, hcb⟩ := hfs hb
    ⟨c, hcs, hcb.symm ▸ hb, hcb.le⟩

Premises used: _private.0.StrictMonoOn.continuousWithinAt_right_of_surjOn.match_1, Set.Ioc, Membership.mem, Exists, Eq.rec, Eq.le, StrictMonoOn.continuousWithinAt_right_of_exists_between, And, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≤] a
hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
h_mono.dual.continuousWithinAt_right_of_exists_between hs fun b hb =>
    let ⟨c, hcs, hcb, hca⟩ := hfs b hb
    ⟨c, hcs, hca, hcb⟩

Premises used: OrderDual.toDual, Set.Ioc, OrderDual.ofDual, setOf, Function.comp, Membership.mem, Exists, StrictMonoOn.continuousWithinAt_right_of_exists_between, And, And.intro, Exists.intro, _private.0.StrictMonoOn.continuousWithinAt_left_of_exists_between.match_1, Set.Iic, OrderDual, DFunLike.coe, StrictMonoOn.dual
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
hf : MonotoneOn f s
hs : s ∈ 𝓝[≤] a
hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
@continuousWithinAt_right_of_monotoneOn_of_exists_between αᵒᵈ βᵒᵈ _ _ _ _ _ _ f s a hf.dual hs
    fun b hb =>
    let ⟨c, hcs, hcb, hca⟩ := hfs b hb
    ⟨c, hcs, hca, hcb⟩

Premises used: setOf, Membership.mem, Exists, continuousWithinAt_right_of_monotoneOn_of_exists_between, And, MonotoneOn.dual, And.intro, Exists.intro, Set.Iic, OrderDual, Set.Ioo, _private.0.continuousWithinAt_left_of_monotoneOn_of_exists_between.match_1
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
hf : MonotoneOn f s
hs : s ∈ 𝓝[≤] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≤] f a
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
@continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ f s
    a hf.dual hs hfs

Premises used: setOf, MonotoneOn.dual, continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≤] a
hfs : f '' s ∈ 𝓝[≤] f a
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin h_mono hs
    (mem_of_superset hfs subset_closure)

Premises used: subset_closure, continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≤] a
hfs : closure[inst_4] (f '' s) ∈ 𝓝[≤] f a
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
h_mono.dual.continuousWithinAt_right_of_closure_image_mem_nhdsWithin hs hfs

Premises used: StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin, setOf, Set.Iic, OrderDual, StrictMonoOn.dual
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≤] a
hfs : f '' s ∈ 𝓝[≤] f a
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
h_mono.dual.continuousWithinAt_right_of_image_mem_nhdsWithin hs hfs

Premises used: StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin, setOf, Set.Iic, OrderDual, StrictMonoOn.dual
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≤] a
hfs : SurjOn f s (Iio (f a))
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
h_mono.dual.continuousWithinAt_right_of_surjOn hs hfs

Premises used: StrictMonoOn.continuousWithinAt_right_of_surjOn, setOf, Set.Iic, OrderDual, StrictMonoOn.dual
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝 a
hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)
hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
⊢ ContinuousAt f a

Tactic:
continuousAt_iff_continuous_left_right.2
    ⟨h_mono.continuousWithinAt_left_of_exists_between (mem_nhdsWithin_of_mem_nhds hs) hfs_l,
      h_mono.continuousWithinAt_right_of_exists_between (mem_nhdsWithin_of_mem_nhds hs) hfs_r⟩

Premises used: Iff.mpr, StrictMonoOn.continuousWithinAt_left_of_exists_between, StrictMonoOn.continuousWithinAt_right_of_exists_between, continuousAt_iff_continuous_left_right, mem_nhdsWithin_of_mem_nhds, And.intro
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝 a
hfs : closure[inst_4] (f '' s) ∈ 𝓝 (f a)
⊢ ContinuousAt f a

Tactic:
continuousAt_iff_continuous_left_right.2
    ⟨h_mono.continuousWithinAt_left_of_closure_image_mem_nhdsWithin (mem_nhdsWithin_of_mem_nhds hs)
        (mem_nhdsWithin_of_mem_nhds hfs),
      h_mono.continuousWithinAt_right_of_closure_image_mem_nhdsWithin
        (mem_nhdsWithin_of_mem_nhds hs) (mem_nhdsWithin_of_mem_nhds hfs)⟩

Premises used: Iff.mpr, StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin, continuousAt_iff_continuous_left_right, mem_nhdsWithin_of_mem_nhds, And.intro, StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
inst_6 : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝 a
hfs : f '' s ∈ 𝓝 (f a)
⊢ ContinuousAt f a

Tactic:
h_mono.continuousAt_of_closure_image_mem_nhds hs (mem_of_superset hfs subset_closure)

Premises used: subset_closure, StrictMonoOn.continuousAt_of_closure_image_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.MonotoneContinuity
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝 a
hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)
hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
⊢ ContinuousAt f a

Tactic:
continuousAt_iff_continuous_left_right.2
    ⟨continuousWithinAt_left_of_monotoneOn_of_exists_between h_mono (mem_nhdsWithin_of_mem_nhds hs)
        hfs_l,
      continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono
        (mem_nhdsWithin_of_mem_nhds hs) hfs_r⟩

Premises used: Iff.mpr, continuousWithinAt_right_of_monotoneOn_of_exists_between, continuousAt_iff_continuous_left_right, mem_nhdsWithin_of_mem_nhds, And.intro, continuousWithinAt_left_of_monotoneOn_of_exists_between