-- Mathlib/Topology/Order/ExtendFrom.lean
theorem continuousOn_Ico_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α]
    [OrderTopology α] [TopologicalSpace β] [RegularSpace β] {f : α → β} {a b : α} {la : β}
    (hab : a < b) (hf : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 la)) :
    ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)

Result:
case hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

case hf.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Proof state:
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Ico a b ⊆ closure (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Result:
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Ico a b ⊆ Icc a b

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)

Tactic:
apply continuousOn_extendFrom

Result:
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Ico a b ⊆ closure (Ioo a b)

case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ ∀ x ∈ Ico a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Proof state:
case hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)

Tactic:
use la

Result:
case h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ Tendsto f (𝓝[Ioo x b] x) (𝓝 la)

Proof state:
case hf.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
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⟩

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ Tendsto f (𝓝[Ioo x b] x) (𝓝 la)

Tactic:
simpa [hab]

Result:
no goals

Proof state:
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Ico a b ⊆ Icc a b

Tactic:
exact Ico_subset_Icc_self

Result:
no goals

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ ∀ x ∈ Ico a b, ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)

Tactic:
intro x x_in

Result:
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)