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

case refine'_2
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t) → IsPreconnected s
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t
refine' ⟨fun hs => _, _⟩
case refine'_1.inl
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : TopologicalSpace β
hs : IsPreconnected ∅
⊢ (∃ t, IsPreconnected t ∧ ∅ = inl '' t) ∨ ∃ t, IsPreconnected t ∧ ∅ = inr '' t

case refine'_1.inr
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : Set.Nonempty s
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t
case refine'_1
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t
obtain rfl | h := s.eq_empty_or_nonempty
case refine'_1.inr.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (inl '' t)
h : Set.Nonempty (inl '' t)
⊢ (∃ t_1, IsPreconnected t_1 ∧ inl '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inl '' t = inr '' t_1

case refine'_1.inr.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (inr '' t)
h : Set.Nonempty (inr '' t)
⊢ (∃ t_1, IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inr '' t = inr '' t_1
case refine'_1.inr
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : Set.Nonempty s
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩
no goals
case refine'_1.inl
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : TopologicalSpace β
hs : IsPreconnected ∅
⊢ (∃ t, IsPreconnected t ∧ ∅ = inl '' t) ∨ ∃ t, IsPreconnected t ∧ ∅ = inr '' t
exact Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩
no goals
case refine'_1.inr.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (inl '' t)
h : Set.Nonempty (inl '' t)
⊢ (∃ t_1, IsPreconnected t_1 ∧ inl '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inl '' t = inr '' t_1
exact Or.inl ⟨t, ht.isPreconnected, rfl⟩
no goals
case refine'_1.inr.inr.intro.intro
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (inr '' t)
h : Set.Nonempty (inr '' t)
⊢ (∃ t_1, IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inr '' t = inr '' t_1
exact Or.inr ⟨t, ht.isPreconnected, rfl⟩
case refine'_2.inl.intro.intro
α : Type u
β : Type v
ι : Type ?u.44185
π : ι → Type ?u.44190
inst✝¹ : TopologicalSpace α
s t✝ u v : Set α
inst✝ : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (inl '' t)

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