case refine'_1
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

case refine'_2
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t) → IsConnected s
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsConnected s ↔ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
refine' ⟨fun hs => _, _⟩
case refine'_1.intro.inl
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

case refine'_1.intro.inr
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
case refine'_1
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
obtain ⟨x | x, hx⟩ := hs.nonempty
case refine'_1.intro.inl
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
case refine'_1.intro.inl
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
have h : s ⊆ range Sum.inl :=
  hs.isPreconnected.subset_clopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
case refine'_1.intro.inl.refine'_1
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ IsConnected (inl ⁻¹' s)

case refine'_1.intro.inl.refine'_2
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' (inl ⁻¹' s)
case refine'_1.intro.inl
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
refine' Or.inl ⟨Sum.inl ⁻¹' s, _, _⟩
no goals
case refine'_1.intro.inl.refine'_1
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ IsConnected (inl ⁻¹' s)
exact hs.preimage_of_openMap Sum.inl_injective isOpenMap_inl h
no goals
case refine'_1.intro.inl.refine'_2
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : α
hx : inl x ∈ s
h : s ⊆ range inl
⊢ s = inl '' (inl ⁻¹' s)
exact (image_preimage_eq_of_subset h).symm
case refine'_1.intro.inr
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
case refine'_1.intro.inr
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
have h : s ⊆ range Sum.inr :=
  hs.isPreconnected.subset_clopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
case refine'_1.intro.inr.refine'_1
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ IsConnected (inr ⁻¹' s)

case refine'_1.intro.inr.refine'_2
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' (inr ⁻¹' s)
case refine'_1.intro.inr
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t
refine' Or.inr ⟨Sum.inr ⁻¹' s, _, _⟩
no goals
case refine'_1.intro.inr.refine'_1
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ IsConnected (inr ⁻¹' s)
exact hs.preimage_of_openMap Sum.inr_injective isOpenMap_inr h
no goals
case refine'_1.intro.inr.refine'_2
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsConnected s
x : β
hx : inr x ∈ s
h : s ⊆ range inr
⊢ s = inr '' (inr ⁻¹' s)
exact (image_preimage_eq_of_subset h).symm
case refine'_2.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
⊢ IsConnected (inl '' t)

case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)
case refine'_2
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t) → IsConnected s
rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)
no goals
case refine'_2.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
⊢ IsConnected (inl '' t)
exact ht.image _ continuous_inl.continuousOn
no goals
case refine'_2.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.42555
π : ι → Type ?u.42560
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)
exact ht.image _ continuous_inr.continuousOn