Theorem: IsPreconnected.limits_Ioc (Ray/Misc/Connected.lean)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
by_cases ab : ¬a < b
State after:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
simp only [not_not] at ab
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
generalize hs : (fun t : Ioc a b ↦ closure (r '' Ioc a t)) = s
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have n : Nonempty (Ioc a b) := ⟨b, right_mem_Ioc.mpr ab⟩
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have m : Monotone s := by
  intro a b ab; rw [← hs]; refine closure_mono (monotone_image ?_)
  exact Ioc_subset_Ioc (le_refl _) (Subtype.coe_le_coe.mpr ab)
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have d : Directed Superset s := fun a b ↦ ⟨min a b, m (min_le_left _ _), m (min_le_right _ _)⟩
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have p : ∀ t, IsPreconnected (s t) := by
  intro ⟨t, m⟩; rw [← hs]; refine (isPreconnected_Ioc.image _ (rc.mono ?_)).closure
  simp only [mem_Ioc] at m
  simp only [Subtype.coe_mk, Ioc_subset_Ioc_iff m.1, m.2, le_refl, true_and_iff]
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
have c : ∀ t, IsCompact (s t) := by intro t; rw [← hs]; exact isClosed_closure.isCompact
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
rw [e]
State after:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
⊢ IsPreconnected (⋂ t, s t)

State before:
case neg
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
e : {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
⊢ IsPreconnected (⋂ t, s t)
Tactic:
exact IsPreconnected.directed_iInter d p c
State after:
no goals

State before:
case pos
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : ¬a < b
⊢ IsPreconnected {x | MapClusterPt x (𝓝[Ioc a b] a) r}
Tactic:
simp only [Ioc_eq_empty ab, nhdsWithin_empty, MapClusterPt, Filter.map_bot, ClusterPt.bot,
  setOf_false, isPreconnected_empty]
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
⊢ Monotone s
Tactic:
intro a b ab
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a✝ b✝ : ℝ
rc : ContinuousOn r (Ioc a✝ b✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ s a ≤ s b

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a✝ b✝ : ℝ
rc : ContinuousOn r (Ioc a✝ b✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ s a ≤ s b
Tactic:
rw [← hs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a✝ b✝ : ℝ
rc : ContinuousOn r (Ioc a✝ b✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ (fun t => closure (r '' Ioc a✝ ↑t)) a ≤ (fun t => closure (r '' Ioc a✝ ↑t)) b

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a✝ b✝ : ℝ
rc : ContinuousOn r (Ioc a✝ b✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ (fun t => closure (r '' Ioc a✝ ↑t)) a ≤ (fun t => closure (r '' Ioc a✝ ↑t)) b
Tactic:
refine closure_mono (monotone_image ?_)
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a✝ b✝ : ℝ
rc : ContinuousOn r (Ioc a✝ b✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ Ioc a✝ ↑a ≤ Ioc a✝ ↑b

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a✝ b✝ : ℝ
rc : ContinuousOn r (Ioc a✝ b✝)
ab✝ : a✝ < b✝
s : ↑(Ioc a✝ b✝) → Set X
hs : (fun t => closure (r '' Ioc a✝ ↑t)) = s
n : Nonempty ↑(Ioc a✝ b✝)
a b : ↑(Ioc a✝ b✝)
ab : a ≤ b
⊢ Ioc a✝ ↑a ≤ Ioc a✝ ↑b
Tactic:
exact Ioc_subset_Ioc (le_refl _) (Subtype.coe_le_coe.mpr ab)
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
⊢ ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
Tactic:
intro ⟨t, m⟩
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected (s ⟨t, m⟩)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected (s ⟨t, m⟩)
Tactic:
rw [← hs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected ((fun t => closure (r '' Ioc a ↑t)) ⟨t, m⟩)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
t : ℝ
m : t ∈ Ioc a b
⊢ IsPreconnected ((fun t => closure (r '' Ioc a ↑t)) ⟨t, m⟩)
Tactic:
refine (isPreconnected_Ioc.image _ (rc.mono ?_)).closure
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
t : ℝ
m : t ∈ Ioc a b
⊢ Ioc a ↑⟨t, m⟩ ⊆ Ioc a b

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
t : ℝ
m : t ∈ Ioc a b
⊢ Ioc a ↑⟨t, m⟩ ⊆ Ioc a b
Tactic:
simp only [mem_Ioc] at m
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝¹ : Monotone s
d : Directed Superset s
t : ℝ
m✝ : t ∈ Ioc a b
m : a < t ∧ t ≤ b
⊢ Ioc a ↑⟨t, m✝⟩ ⊆ Ioc a b

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝¹ : Monotone s
d : Directed Superset s
t : ℝ
m✝ : t ∈ Ioc a b
m : a < t ∧ t ≤ b
⊢ Ioc a ↑⟨t, m✝⟩ ⊆ Ioc a b
Tactic:
simp only [Subtype.coe_mk, Ioc_subset_Ioc_iff m.1, m.2, le_refl, true_and_iff]
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
⊢ ∀ (t : ↑(Ioc a b)), IsCompact (s t)
Tactic:
intro t
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
t : ↑(Ioc a b)
⊢ IsCompact (s t)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
t : ↑(Ioc a b)
⊢ IsCompact (s t)
Tactic:
rw [← hs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
t : ↑(Ioc a b)
⊢ IsCompact ((fun t => closure (r '' Ioc a ↑t)) t)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
t : ↑(Ioc a b)
⊢ IsCompact ((fun t => closure (r '' Ioc a ↑t)) t)
Tactic:
exact isClosed_closure.isCompact
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
⊢ {x | MapClusterPt x (𝓝[Ioc a b] a) r} = ⋂ t, s t
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
⊢ ∀ (x : X), x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
⊢ ∀ (x : X), x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t
Tactic:
intro x
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
⊢ x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
⊢ x ∈ {x | MapClusterPt x (𝓝[Ioc a b] a) r} ↔ x ∈ ⋂ t, s t
Tactic:
simp only [mem_setOf, mem_iInter, mapClusterPt_iff, mem_closure_iff_nhds, Set.Nonempty,
  @forall_comm _ (Set X), ← hs]
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ s) ↔
    ∀ (b_1 : Set X) (a_1 : ↑(Ioc a b)), b_1 ∈ 𝓝 x → ∃ x, x ∈ b_1 ∩ r '' Ioc a ↑a_1

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ s) ↔
    ∀ (b_1 : Set X) (a_1 : ↑(Ioc a b)), b_1 ∈ 𝓝 x → ∃ x, x ∈ b_1 ∩ r '' Ioc a ↑a_1
Tactic:
apply forall_congr'
State after:
case h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
⊢ ∀ (a_1 : Set X),
    (a_1 ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ a_1) ↔
      ∀ (a_2 : ↑(Ioc a b)), a_1 ∈ 𝓝 x → ∃ x, x ∈ a_1 ∩ r '' Ioc a ↑a_2

State before:
case h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
⊢ ∀ (a_1 : Set X),
    (a_1 ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ a_1) ↔
      ∀ (a_2 : ↑(Ioc a b)), a_1 ∈ 𝓝 x → ∃ x, x ∈ a_1 ∩ r '' Ioc a ↑a_2
Tactic:
intro u
State after:
case h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), u ∈ 𝓝 x → ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1

State before:
case h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), u ∈ 𝓝 x → ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Tactic:
simp only [@forall_comm _ (u ∈ 𝓝 x)]
State after:
case h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ u ∈ 𝓝 x → ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1

State before:
case h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
⊢ (u ∈ 𝓝 x → ∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ u ∈ 𝓝 x → ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Tactic:
apply forall_congr'
State after:
case h.h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
⊢ u ∈ 𝓝 x → ((∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_2 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_2)

State before:
case h.h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
⊢ u ∈ 𝓝 x → ((∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_2 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_2)
Tactic:
intro _
State after:
case h.h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1

State before:
case h.h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∃ᶠ (a : ℝ) in 𝓝[Ioc a b] a, r a ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x, x ∈ u ∩ r '' Ioc a ↑a_1
Tactic:
simp only [mem_inter_iff, Filter.frequently_iff, nhdsWithin_Ioc_eq_nhdsWithin_Ioi ab]
State after:
case h.h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1

State before:
case h.h.h
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u) ↔ ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
Tactic:
constructor
State after:
case h.h.h.mp
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u) → ∀ (a_2 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_2

case h.h.h.mpr
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1) → ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u

State before:
case h.h.h.mp
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u) → ∀ (a_2 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_2
Tactic:
intro h ⟨t, m⟩
State after:
case h.h.h.mp
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩

State before:
case h.h.h.mp
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Tactic:
have tm : Ioc a t ∈ 𝓝[Ioi a] a := by
  apply Ioc_mem_nhdsWithin_Ioi
  simp only [mem_Ioc] at m; simp only [mem_Ico]; use le_refl _, m.1
State after:
case h.h.h.mp
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩

State before:
case h.h.h.mp
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Tactic:
rcases h tm with ⟨v, vm, vu⟩
State after:
case h.h.h.mp.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
v : ℝ
vm : v ∈ Ioc a t
vu : r v ∈ u
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩

State before:
case h.h.h.mp.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
tm : Ioc a t ∈ 𝓝[>] a
v : ℝ
vm : v ∈ Ioc a t
vu : r v ∈ u
⊢ ∃ x ∈ u, x ∈ r '' Ioc a ↑⟨t, m⟩
Tactic:
exact ⟨r v, vu, mem_image_of_mem _ vm⟩
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ Ioc a t ∈ 𝓝[>] a
Tactic:
apply Ioc_mem_nhdsWithin_Ioi
State after:
case H
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ a ∈ Ico a t

State before:
case H
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : t ∈ Ioc a b
⊢ a ∈ Ico a t
Tactic:
simp only [mem_Ioc] at m
State after:
case H
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ∈ Ico a t

State before:
case H
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ∈ Ico a t
Tactic:
simp only [mem_Ico]
State after:
case H
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ≤ a ∧ a < t

State before:
case H
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
t : ℝ
m : a < t ∧ t ≤ b
⊢ a ≤ a ∧ a < t
Tactic:
use le_refl _, m.1
State after:
no goals

State before:
case h.h.h.mpr
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
⊢ (∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1) → ∀ {U : Set ℝ}, U ∈ 𝓝[>] a → ∃ x ∈ U, r x ∈ u
Tactic:
intro h v vm
State after:
case h.h.h.mpr
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
rcases mem_nhdsWithin_Ioi_iff_exists_Ioc_subset.mp vm with ⟨w, wa, wv⟩
State after:
case h.h.h.mpr.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wa : w ∈ Ioi a
wv : Ioc a w ⊆ v
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wa : w ∈ Ioi a
wv : Ioc a w ⊆ v
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
simp only [mem_Ioi] at wa
State after:
case h.h.h.mpr.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
have m : min w b ∈ Ioc a b := by simp only [mem_Ioc]; use lt_min wa ab, min_le_right _ _
State after:
case h.h.h.mpr.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
rcases h ⟨_, m⟩ with ⟨x, xu, rx⟩
State after:
case h.h.h.mpr.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : x ∈ r '' Ioc a ↑⟨min w b, m⟩
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : x ∈ r '' Ioc a ↑⟨min w b, m⟩
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
simp only [Subtype.coe_mk, mem_image, mem_Ioc, le_min_iff] at rx
State after:
case h.h.h.mpr.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : ∃ x_1, (a < x_1 ∧ x_1 ≤ w ∧ x_1 ≤ b) ∧ r x_1 = x
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
rx : ∃ x_1, (a < x_1 ∧ x_1 ≤ w ∧ x_1 ≤ b) ∧ r x_1 = x
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
rcases rx with ⟨c, ⟨ac, cw, _⟩, cx⟩
State after:
case h.h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c✝ : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ ∃ x ∈ v, r x ∈ u

State before:
case h.h.h.mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c✝ : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ ∃ x ∈ v, r x ∈ u
Tactic:
use c, wv (mem_Ioc.mpr ⟨ac, cw⟩)
State after:
case right
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c✝ : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ r c ∈ u

State before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c✝ : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ r c ∈ u
Tactic:
rwa [cx]
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ min w b ∈ Ioc a b
Tactic:
simp only [mem_Ioc]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ a < min w b ∧ min w b ≤ b

State before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ a < min w b ∧ min w b ≤ b
Tactic:
use lt_min wa ab, min_le_right _ _
State after:
no goals