awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
inr : f x ≤ sSup (f '' Iio y)
⊢ f x ≤ leftLim f y

Tactic:
rw [leftLim_eq_sSup hf h']

Premises used: Monotone.leftLim_eq_sSup
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
⊢ f x ≤ sSup (f '' Iio y)

Tactic:
le_csSup ⟨f y, ?_⟩ (mem_image_of_mem _ h)

Premises used: Set.mem_image_of_mem, Exists.intro, le_csSup
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
inr : f y ∈ upperBounds (f '' Iio y)
⊢ f x ≤ sSup (f '' Iio y)

Tactic:
refine le_csSup ⟨f y, ?_⟩ (mem_image_of_mem _ h)

Premises used: Set.mem_image_of_mem, Exists.intro, le_csSup
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
inr : ∀ a < y, f a ≤ f y
⊢ f y ∈ upperBounds (f '' Iio y)

Tactic:
simp only [upperBounds, mem_image, mem_Iio, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, mem_setOf_eq]

Premises used: Set.mem_Iio, and_imp, Set.mem_image, forall_exists_index, upperBounds, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
z : α
hz : z < y
⊢ f z ≤ f y

Tactic:
hf hz.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
z : α
hz : z < y
⊢ f z ≤ f y

Tactic:
exact hf hz.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
inl : ∀ (h : x ≤ x), leftLim f x ≤ leftLim f x
inr : ∀ (hxy : x < y), leftLim f x ≤ leftLim f y
⊢ leftLim f x ≤ leftLim f y

Tactic:
rcases eq_or_lt_of_le h with (rfl | hxy)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
h : x ≤ x
⊢ leftLim f x ≤ leftLim f x

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
h : x ≤ x
⊢ leftLim f x ≤ leftLim f x

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y

Tactic:
(hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)

Premises used: le_rfl, Monotone.leftLim_le, LE.le.trans, Monotone.le_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y

Tactic:
exact (hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)

Premises used: le_rfl, Monotone.leftLim_le, LE.le.trans, Monotone.le_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ f x ≤ rightLim f y

Tactic:
hf.dual.leftLim_le h

Premises used: Monotone.dual, Function.rightLim, Monotone.leftLim_le, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ rightLim f x ≤ f y

Tactic:
hf.dual.le_leftLim h

Premises used: Monotone.dual, Function.rightLim, OrderDual, Monotone.le_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
⊢ Monotone (rightLim f)

Tactic:
fun _ _ h => hf.dual.leftLim h

Premises used: Monotone.leftLim, Monotone, Monotone.dual, Function.rightLim, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ rightLim f y

Tactic:
(hf.leftLim_le le_rfl).trans (hf.le_rightLim h)

Premises used: le_rfl, Monotone.le_rightLim, Monotone.leftLim_le, LE.le.trans
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
inl : ∀ (h' : 𝓝[<] y = ⊥), rightLim f x ≤ leftLim f y
inr : ∀ (h' : (𝓝[<] y).NeBot), rightLim f x ≤ leftLim f y
⊢ rightLim f x ≤ leftLim f y

Tactic:
rcases eq_or_neBot (𝓝[<] y) with (h' | h')

Premises used: nhdsWithin, Filter.eq_or_neBot, Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
⊢ rightLim f x ≤ leftLim f y

Tactic:
simpa [leftLim, h'] using rightLim_le hf h

Premises used: Monotone.rightLim_le, Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ (Ioo x y).Nonempty

Tactic:
nonempty_of_mem (Ioo_mem_nhdsLT h)

Premises used: Filter.nonempty_of_mem, Ioo_mem_nhdsLT
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
inr : ∀ (a : α) (xa : x < a) (ay : a < y), rightLim f x ≤ leftLim f y
⊢ rightLim f x ≤ leftLim f y

Tactic:
obtain ⟨a, ⟨xa, ay⟩⟩ : (Ioo x y).Nonempty := nonempty_of_mem (Ioo_mem_nhdsLT h)

Premises used: Set.Nonempty, Set.Ioo
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
a : α
xa : x < a
ay : a < y
⊢ rightLim f x ≤ f a

Tactic:
hf.rightLim_le xa

Premises used: Monotone.rightLim_le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
a : α
xa : x < a
ay : a < y
⊢ f a ≤ leftLim f y

Tactic:
hf.le_leftLim ay

Premises used: Monotone.le_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
a : α
xa : x < a
ay : a < y
⊢ rightLim f x ≤ leftLim f y

Tactic:
calc
    rightLim f x ≤ f a := hf.rightLim_le xa
    _ ≤ leftLim f y := hf.le_leftLim ay

Premises used: Monotone.rightLim_le, Function.rightLim, Monotone.le_leftLim, Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Tactic:
tendsto_leftLim_of_tendsto ⟨_, hf.tendsto_nhdsLT x⟩

Premises used: tendsto_leftLim_of_tendsto, Monotone.tendsto_nhdsLT, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
apply : ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)
⊢ Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f (hf.tendsto_leftLim x)

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Monotone.tendsto_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x y : α
hy : y ∈ Iio x
⊢ f y ∈ Iic (leftLim f x)

Tactic:
hf.le_leftLim hy

Premises used: Set.Mem, setOf, Set.Iic, Monotone.le_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        x_1 ∈ Iio x → Membership.mem (γ := Set α) {x_2 : α | (fun (x_3 : α) ↦ f x_3 ∈ Iic (leftLim f x)) x_2} x_1}
      a
h₁ h₂ : ∀ (y : α) (hy : y ∈ Iio x), f y ∈ Iic (leftLim f x)
⊢ ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)

Tactic:
filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝 (rightLim f x))

Tactic:
hf.dual.tendsto_leftLim x

Premises used: Set.Ioi, setOf, Monotone.dual, Function.rightLim, OrderDual, Monotone.tendsto_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝[≥] rightLim f x)

Tactic:
hf.dual.tendsto_leftLim_within x

Premises used: Set.Ioi, Set.Ici, setOf, Monotone.dual, Function.rightLim, Monotone.tendsto_leftLim_within, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
inl : ∀ (h' : 𝓝[<] x = ⊥), ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
inr : ∀ (h' : 𝓝[<] x ≠ ⊥), ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')

Premises used: nhdsWithin, Bot.bot, eq_or_ne, Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h']

Premises used: leftLim_eq_of_eq_bot, ContinuousWithinAt
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
⊢ (𝓝[<] x).NeBot

Tactic:
haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h'
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩

Premises used: Iff.intro, ContinuousWithinAt.tendsto, tendsto_nhds_unique, Monotone.tendsto_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
inr : ∀ (h : leftLim f x = f x), ContinuousWithinAt f (Iio x) x
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
refine ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
h : leftLim f x = f x
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Tactic:
have := hf.tendsto_leftLim x
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this_1 : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
inr inr₁ inr₂ inr₃ : ∀ (this : Tendsto f (𝓝[<] x) (𝓝 (f x))), ContinuousWithinAt f (Iio x) x
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
rwa [h] at this
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousWithinAt f (Ioi x) x ↔ rightLim f x = f x

Tactic:
hf.dual.continuousWithinAt_Iio_iff_leftLim_eq

Premises used: Set.Ioi, setOf, Monotone.continuousWithinAt_Iio_iff_leftLim_eq, Monotone.dual, Function.rightLim, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
refine_1 : ∀ (h : ContinuousAt f x), leftLim f x = rightLim f x
refine_2 : ∀ (h : leftLim f x = rightLim f x), ContinuousAt f x
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : ContinuousAt f x
⊢ leftLim f x = f x

Tactic:
have A : leftLim f x = f x :=
      hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
⊢ rightLim f x = f x

Tactic:
have B : rightLim f x = f x :=
      hf.continuousWithinAt_Ioi_iff_rightLim_eq.1 h.continuousWithinAt
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
B : rightLim f x = f x
⊢ leftLim f x = rightLim f x

Tactic:
A.trans B.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
B : rightLim f x = f x
⊢ leftLim f x = rightLim f x

Tactic:
exact A.trans B.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
apply : f x ≤ leftLim f x
⊢ leftLim f x = f x

Tactic:
apply le_antisymm (leftLim_le hf (le_refl _))

Premises used: le_refl, le_antisymm, Monotone.leftLim_le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
rw : f x ≤ rightLim f x
⊢ f x ≤ leftLim f x

Tactic:
rw [h]
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ rightLim f x

Tactic:
le_rightLim hf (le_refl _)

Premises used: le_refl, Monotone.le_rightLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ rightLim f x

Tactic:
exact le_rightLim hf (le_refl _)

Premises used: le_refl, Monotone.le_rightLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
⊢ leftLim f x = f x

Tactic:
have h' : leftLim f x = f x := by
      apply le_antisymm (leftLim_le hf (le_refl _))
      rw [h]
      exact le_rightLim hf (le_refl _)
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousAt f x

Tactic:
continuousAt_iff_continuous_left'_right'.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, continuousAt_iff_continuous_left'_right', And.intro
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
refine_2 : ContinuousWithinAt f (Iio x) x
refine_2₁ : ContinuousWithinAt f (Ioi x) x
⊢ ContinuousAt f x

Tactic:
refine continuousAt_iff_continuous_left'_right'.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, continuousAt_iff_continuous_left'_right', And.intro
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'

Premises used: Iff.mpr, Monotone.continuousWithinAt_Iio_iff_leftLim_eq
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
exact hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'

Premises used: Iff.mpr, Monotone.continuousWithinAt_Iio_iff_leftLim_eq
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ rightLim f x = f x

Tactic:
rw [h] at h'