case pos
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

case neg
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : ¬x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
by_cases hx : x ∈ F
case pos
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ Subtype.val '' (inclusion h '' connectedComponent { val := x, property := hx }) ⊆
    Subtype.val '' connectedComponent { val := x, property := (_ : x ∈ G) }
case pos
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
rw [connectedComponentIn_eq_image hx, connectedComponentIn_eq_image (h hx), ←
  show ((↑) : G → α) ∘ inclusion h = (↑) from rfl, image_comp]
no goals
case pos
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ Subtype.val '' (inclusion h '' connectedComponent { val := x, property := hx }) ⊆
    Subtype.val '' connectedComponent { val := x, property := (_ : x ∈ G) }
exact image_subset _ ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩)
case neg
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : ¬x ∈ F
⊢ ∅ ⊆ connectedComponentIn G x
case neg
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : ¬x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x
rw [connectedComponentIn_eq_empty hx]
no goals
case neg
α : Type u
β : Type v
ι : Type ?u.59761
π : ι → Type ?u.59766
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F G : Set α
h : F ⊆ G
hx : ¬x ∈ F
⊢ ∅ ⊆ connectedComponentIn G x
exact Set.empty_subset _