-- Mathlib/Topology/Connected/Clopen.lean
theorem Sum.isPreconnected_iff [TopologicalSpace β] {s : Set (α ⊕ β)} :
    IsPreconnected s ↔
      (∃ t, IsPreconnected t ∧ s = Sum.inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = Sum.inr '' t

Proof state:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Result:
case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
hs : IsPreconnected ∅
⊢ (∃ t, IsPreconnected t ∧ ∅ = inl '' t) ∨ ∃ t, IsPreconnected t ∧ ∅ = inr '' t

case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : s.Nonempty
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Proof state:
case refine_2.inl.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (inl '' t)

Tactic:
exact ht.image _ continuous_inl.continuousOn

Result:
no goals

Proof state:
case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : s.Nonempty
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isConnected_iff.1 ⟨h, hs⟩

Result:
case refine_1.inr.inl.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (inl '' t)
h : (inl '' t).Nonempty
⊢ (∃ 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
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (inr '' t)
h : (inr '' t).Nonempty
⊢ (∃ t_1, IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inr '' t = inr '' t_1

Proof state:
case refine_1.inr.inr.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
hs : IsPreconnected (inr '' t)
h : (inr '' t).Nonempty
⊢ (∃ t_1, IsPreconnected t_1 ∧ inr '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inr '' t = inr '' t_1

Tactic:
exact Or.inr ⟨t, ht.isPreconnected, rfl⟩

Result:
no goals

Proof state:
case refine_1.inr.inl.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsConnected t
hs : IsPreconnected (inl '' t)
h : (inl '' t).Nonempty
⊢ (∃ t_1, IsPreconnected t_1 ∧ inl '' t = inl '' t_1) ∨ ∃ t_1, IsPreconnected t_1 ∧ inl '' t = inr '' t_1

Tactic:
exact Or.inl ⟨t, ht.isPreconnected, rfl⟩

Result:
no goals

Proof state:
case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t) → IsPreconnected s

Tactic:
rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)

Result:
case refine_2.inl.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set α
ht : IsPreconnected t
⊢ IsPreconnected (inl '' t)

case refine_2.inr.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)

Proof state:
case refine_2.inr.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)

Tactic:
exact ht.image _ continuous_inr.continuousOn

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsPreconnected s ↔ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩

Result:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
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
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t) → IsPreconnected s

Proof state:
case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
hs : IsPreconnected ∅
⊢ (∃ t, IsPreconnected t ∧ ∅ = inl '' t) ∨ ∃ t, IsPreconnected t ∧ ∅ = inr '' t

Tactic:
exact Or.inl ⟨∅, isPreconnected_empty, (Set.image_empty _).symm⟩

Result:
no goals