-- Mathlib/Topology/Connected/Clopen.lean
theorem Sigma.isPreconnected_iff [hι : Nonempty ι] [∀ i, TopologicalSpace (π i)]
    {s : Set (Σi, π i)} : IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = Sigma.mk i '' t

Proof state:
case refine_1
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsPreconnected s
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Result:
case refine_1.inl
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
hs : IsPreconnected ∅
⊢ ∃ i t, IsPreconnected t ∧ ∅ = mk i '' t

case refine_1.inr
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsPreconnected s
h : s.Nonempty
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Proof state:
case refine_1.inl
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
hs : IsPreconnected ∅
⊢ ∃ i t, IsPreconnected t ∧ ∅ = mk i '' t

Tactic:
exact ⟨Classical.choice hι, ∅, isPreconnected_empty, (Set.image_empty _).symm⟩

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
⊢ IsPreconnected s ↔ ∃ i t, IsPreconnected t ∧ s = mk i '' t

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

Result:
case refine_1
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsPreconnected s
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t

case refine_2
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
⊢ (∃ i t, IsPreconnected t ∧ s = mk i '' t) → IsPreconnected s

Proof state:
case refine_2.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
a : ι
t : Set (π a)
ht : IsPreconnected t
⊢ IsPreconnected (mk a '' t)

Tactic:
exact ht.image _ continuous_sigmaMk.continuousOn

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
⊢ (∃ i t, IsPreconnected t ∧ s = mk i '' t) → IsPreconnected s

Tactic:
rintro ⟨a, t, ht, rfl⟩

Result:
case refine_2.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
a : ι
t : Set (π a)
ht : IsPreconnected t
⊢ IsPreconnected (mk a '' t)

Proof state:
case refine_1.inr
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
s : Set ((i : ι) × π i)
hs : IsPreconnected s
h : s.Nonempty
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Tactic:
obtain ⟨a, t, ht, rfl⟩ := Sigma.isConnected_iff.1 ⟨h, hs⟩

Result:
case refine_1.inr.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
a : ι
t : Set (π a)
ht : IsConnected t
hs : IsPreconnected (mk a '' t)
h : (mk a '' t).Nonempty
⊢ ∃ i t_1, IsPreconnected t_1 ∧ mk a '' t = mk i '' t_1

Proof state:
case refine_1.inr.intro.intro.intro
ι : Type u_1
π : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (π i)
a : ι
t : Set (π a)
ht : IsConnected t
hs : IsPreconnected (mk a '' t)
h : (mk a '' t).Nonempty
⊢ ∃ i t_1, IsPreconnected t_1 ∧ mk a '' t = mk i '' t_1

Tactic:
exact ⟨a, t, ht.isPreconnected, rfl⟩

Result:
no goals