Theorem: local_preconnected_nhdsSet (Ray/Misc/Topology.lean)

State before:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : s ∈ 𝓝ˢ t
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Tactic:
rw [← subset_interior_iff_mem_nhdsSet] at st
State after:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c

State before:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Tactic:
have hsub : t ⊆ ⋃ x : t, connectedComponentIn (interior s) x := fun x hx ↦
  mem_iUnion.2 ⟨⟨x, hx⟩, mem_connectedComponentIn (st hx)⟩
State after:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c

State before:
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∃ c, IsOpen c ∧ t ⊆ c ∧ c ⊆ s ∧ IsPreconnected c
Tactic:
refine ⟨_, isOpen_iUnion fun _ ↦ isOpen_interior.connectedComponentIn, hsub,
  iUnion_subset fun x ↦ ?_, ?_⟩
State after:
case refine_1
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
x : ↑t
⊢ connectedComponentIn (interior s) ↑x ⊆ s

case refine_2
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ IsPreconnected (⋃ i, connectedComponentIn (interior s) ↑i)

State before:
case refine_1
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
x : ↑t
⊢ connectedComponentIn (interior s) ↑x ⊆ s
Tactic:
exact (connectedComponentIn_subset _ _).trans interior_subset
State after:
no goals

State before:
case refine_2
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ IsPreconnected (⋃ i, connectedComponentIn (interior s) ↑i)
Tactic:
apply IsPreconnected.iUnion_of_pairwise_exists_isPreconnected
State after:
case refine_2.hsc
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∀ (i : ↑t), IsPreconnected (connectedComponentIn (interior s) ↑i)

case refine_2.h
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ Pairwise fun i j =>
    (connectedComponentIn (interior s) ↑i).Nonempty →
      (connectedComponentIn (interior s) ↑j).Nonempty →
        ∃ u ⊆ ⋃ i, connectedComponentIn (interior s) ↑i,
          (connectedComponentIn (interior s) ↑i ∩ u).Nonempty ∧
            (u ∩ connectedComponentIn (interior s) ↑j).Nonempty ∧ IsPreconnected u

State before:
case refine_2.hsc
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ ∀ (i : ↑t), IsPreconnected (connectedComponentIn (interior s) ↑i)
Tactic:
exact fun _ ↦ isPreconnected_connectedComponentIn
State after:
no goals

State before:
case refine_2.h
X : Type
inst✝ : TopologicalSpace X
lc : LocallyConnectedSpace X
s t : Set X
tc : IsPreconnected t
st : t ⊆ interior s
hsub : t ⊆ ⋃ x, connectedComponentIn (interior s) ↑x
⊢ Pairwise fun i j =>
    (connectedComponentIn (interior s) ↑i).Nonempty →
      (connectedComponentIn (interior s) ↑j).Nonempty →
        ∃ u ⊆ ⋃ i, connectedComponentIn (interior s) ↑i,
          (connectedComponentIn (interior s) ↑i ∩ u).Nonempty ∧
            (u ∩ connectedComponentIn (interior s) ↑j).Nonempty ∧ IsPreconnected u
Tactic:
exact fun x y _ _ _ ↦ ⟨t, hsub, ⟨x, mem_connectedComponentIn (st x.2), x.2⟩,
  ⟨y, y.2, mem_connectedComponentIn (st y.2)⟩, tc⟩
State after:
no goals