awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a = b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
simp [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
neg : ∀ (hab' : a < b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
neg₁ : ∀ (hba' : b < a), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
obtain hab' | hba' := hab.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hab' : a < b
neg :
  ∀ (ha : Tendsto f (𝓝[>] a) (𝓝 la)) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) (hf : ContinuousOn f (Ioo a b)),
    ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
simp only [hab', uIoo_of_lt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
      uIcc_of_lt] at ha hb hf ⊢

Premises used: nhdsWithin_Ioo_eq_nhdsLT, Set.uIcc_of_lt, Set.uIoo_of_lt, nhdsWithin_Ioo_eq_nhdsGT
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hab : a ≠ b
hab' : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hf : ContinuousOn f (Ioo a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
continuousOn_Icc_extendFrom_Ioo hf ha hb

Premises used: continuousOn_Icc_extendFrom_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hab : a ≠ b
hab' : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hf : ContinuousOn f (Ioo a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)

Tactic:
exact continuousOn_Icc_extendFrom_Ioo hf ha hb

Premises used: continuousOn_Icc_extendFrom_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
neg :
  ∀ (ha : Tendsto f (𝓝[<] a) (𝓝 la)) (hb : Tendsto f (𝓝[>] b) (𝓝 lb)) (hf : ContinuousOn f (Ioo b a)),
    ContinuousOn (extendFrom (Ioo b a) f) (Icc b a)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)

Tactic:
simp only [hba', uIoo_of_gt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
      uIcc_of_gt] at ha hb hf ⊢

Premises used: nhdsWithin_Ioo_eq_nhdsLT, Set.uIoo_of_gt, nhdsWithin_Ioo_eq_nhdsGT, Set.uIcc_of_gt
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hab : a ≠ b
hba' : b < a
ha : Tendsto f (𝓝[<] a) (𝓝 la)
hb : Tendsto f (𝓝[>] b) (𝓝 lb)
hf : ContinuousOn f (Ioo b a)
⊢ ContinuousOn (extendFrom (Ioo b a) f) (Icc b a)

Tactic:
continuousOn_Icc_extendFrom_Ioo hf hb ha

Premises used: continuousOn_Icc_extendFrom_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hab : a ≠ b
hba' : b < a
ha : Tendsto f (𝓝[<] a) (𝓝 la)
hb : Tendsto f (𝓝[>] b) (𝓝 lb)
hf : ContinuousOn f (Ioo b a)
⊢ ContinuousOn (extendFrom (Ioo b a) f) (Icc b a)

Tactic:
exact continuousOn_Icc_extendFrom_Ioo hf hb ha

Premises used: continuousOn_Icc_extendFrom_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
pos : ∀ (hab : a ≥ b), ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
neg : ∀ (hab : a < b), ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

Tactic:
by_cases! hab : a ≥ b
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a ≥ b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

Tactic:
simp [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
neg : Ico a b ⊆ closure[inst] (Ioo a b)
neg₁ : ∀ x ∈ Ico a b, ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

Tactic:
apply continuousOn_extendFrom

Premises used: continuousOn_extendFrom
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
neg : Ico a b ⊆ Icc a b
⊢ Ico a b ⊆ closure[inst] (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Premises used: LT.lt.ne, closure_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ Ico a b ⊆ Icc a b

Tactic:
Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ Ico a b ⊆ Icc a b

Tactic:
exact Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
neg :
  ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x < b) (x_in : x ∈ Ico x b),
    ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
neg₁ : ∀ (h : x ∈ Ioo a b), ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)

Premises used: Set.eq_left_or_mem_Ioo_of_mem_Ico, rfl
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
b : α
la : β
inst_5 : RegularSpace β
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x < b
x_in : x ∈ Ico x b
h : Tendsto f (𝓝[Ioo x b] x) (𝓝 la)
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

Tactic:
use la
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
b : α
la : β
inst_5 : RegularSpace β
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x < b
x_in : x ∈ Ico x b
⊢ Tendsto f (𝓝[Ioo x b] x) (𝓝 la)

Tactic:
simpa [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
⟨f x, hf x h⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
exact ⟨f x, hf x h⟩
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ ∀
    (hf :
      ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ))
    (ha :
      Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (𝓝[>] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
    ContinuousOn (X := αᵒᵈ)
      (extendFrom (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a))
          (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) :
        αᵒᵈ → β)
      (Ico ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)

Tactic:
have := continuousOn_Ico_extendFrom_Ioo (f := f ∘ OrderDual.ofDual) (a := OrderDual.toDual b)
    (b := OrderDual.toDual a) (la := lb)
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ∀
    (hf :
      ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ))
    (ha :
      Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (𝓝[>] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
    ContinuousOn (X := αᵒᵈ)
      (extendFrom (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a))
          (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) :
        αᵒᵈ → β)
      (Ico ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)
⊢ ∀
    (hf :
      ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α))
        ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b))
    (ha :
      Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (𝓝[(⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Iio b] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
    ContinuousOn (X := αᵒᵈ)
      (extendFrom ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)))
      ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc a b)

Tactic:
rw [Ico_toDual, Ioi_toDual, Ioo_toDual] at this

Premises used: Set.Ico_toDual, Set.Ioo_toDual, Set.Ioi_toDual
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ∀
    (hf :
      ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α))
        ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b))
    (ha :
      Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (𝓝[(⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Iio b] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
    ContinuousOn (X := αᵒᵈ)
      (extendFrom ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)))
      ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
this hf hb

Premises used: Set.Ioc, Set.Mem, setOf, Set.preimage, OrderDual, Set.Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ∀
    (hf :
      ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α))
        ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b))
    (ha :
      Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
        (𝓝[(⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Iio b] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
    ContinuousOn (X := αᵒᵈ)
      (extendFrom ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioo a b) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)))
      ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
exact this hf hb
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hx : a ∈ closure[inst] (Ioo a b)
hf : Tendsto f (𝓝[Ioo a b] a) (𝓝 la)
⊢ extendFrom (Ioo a b) f a = la

Tactic:
apply extendFrom_eq

Premises used: extendFrom_eq
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hx : a ∈ Icc a b
⊢ a ∈ closure[inst] (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Premises used: LT.lt.ne, closure_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ Icc a b

Tactic:
simp only [le_of_lt hab, left_mem_Icc]

Premises used: le_of_lt, Set.left_mem_Icc
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Tendsto f (𝓝[Ioo a b] a) (𝓝 la)

Tactic:
simpa [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hx : b ∈ closure[inst] (Ioo a b)
hf : Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)
⊢ extendFrom (Ioo a b) f b = lb

Tactic:
apply extendFrom_eq

Premises used: extendFrom_eq
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hx : b ∈ Icc a b
⊢ b ∈ closure[inst] (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Premises used: LT.lt.ne, closure_Ioo
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ Icc a b

Tactic:
simp only [le_of_lt hab, right_mem_Icc]

Premises used: Set.right_mem_Icc, le_of_lt
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)

Tactic:
simpa [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : T2Space β
hab : a ≠ b
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
⊢ a ∈ closure[inst] (uIoo a b)

Tactic:
simp [hab]
-- Module: Mathlib.Topology.Order.ExtendFrom
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : T2Space β
hab : a ≠ b
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
⊢ b ∈ closure[inst] (uIoo a b)

Tactic:
simp [hab]
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
rw : ∀ (a : β), IsOpen (f ⁻¹' Ioi a) ∧ IsOpen (f ⁻¹' Iio a)
⊢ Continuous f

Tactic:
rw [OrderTopology.continuous_iff]

Premises used: OrderTopology.continuous_iff
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
⊢ ∀ (a : β), IsOpen (f ⁻¹' Ioi a) ∧ IsOpen (f ⁻¹' Iio a)

Tactic:
fun b ↦ ⟨?_, ((isLowerSet_Iio b).preimage hf.strictMono.monotone).isOpen⟩

Premises used: StrictMono.monotone, IsLowerSet.preimage, IsLowerSet.isOpen, isLowerSet_Iio, And.intro, Order.IsNormal.strictMono
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
refine : ∀ (b : β), IsOpen (f ⁻¹' Ioi b)
⊢ ∀ (a : β), IsOpen (f ⁻¹' Ioi a) ∧ IsOpen (f ⁻¹' Iio a)

Tactic:
refine fun b ↦ ⟨?_, ((isLowerSet_Iio b).preimage hf.strictMono.monotone).isOpen⟩
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
rw : IsClosed (f ⁻¹' Iic b)
⊢ IsOpen (f ⁻¹' Ioi b)

Tactic:
rw [← isClosed_compl_iff, ← Set.preimage_compl, Set.compl_Ioi]

Premises used: Set.compl_Ioi, Set.preimage_compl, isClosed_compl_iff
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
inl : ∀ (ha : f ⁻¹' Iic b = univ), IsClosed (f ⁻¹' Iic b)
inr : ∀ (a : α) (ha : f ⁻¹' Iic b = Iio a), IsClosed (f ⁻¹' Iic b)
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
obtain ha | ⟨a, ha⟩ := ((isLowerSet_Iic b).preimage hf.strictMono.monotone).eq_univ_or_Iio

Premises used: IsLowerSet.eq_univ_or_Iio, StrictMono.monotone, IsLowerSet.preimage, Order.IsNormal.strictMono, isLowerSet_Iic
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
ha : f ⁻¹' Iic b = univ
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
ha ▸ isClosed_univ

Premises used: isClosed_univ, Eq.rec, Eq.symm
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
ha : f ⁻¹' Iic b = univ
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
exact ha ▸ isClosed_univ
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
inr : ∀ (h : f ⁻¹' Iic b = ∅), IsClosed (f ⁻¹' Iic b)
inr₁ : ∀ (h : (f ⁻¹' Iic b).Nonempty), IsClosed (f ⁻¹' Iic b)
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
obtain h | h := (f ⁻¹' Iic b).eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, Set.preimage, Set.Iic
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : f ⁻¹' Iic b = ∅
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
h ▸ isClosed_empty

Premises used: Eq.rec, isClosed_empty, Eq.symm
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : f ⁻¹' Iic b = ∅
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
exact h ▸ isClosed_empty
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩