-- Mathlib/Topology/Connected/Clopen.lean
theorem Continuous.exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpace (π i)]
    {f : α → Σ i, π i} (hf : Continuous f) :
    ∃ (i : ι) (g : α → π i), Continuous g ∧ f = Sigma.mk i ∘ g

Proof state:
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) × π i
hf : Continuous f
⊢ ∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g

Tactic:
obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by
  rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
  exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩

Result:
case intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) × π i
hf : Continuous f
i : ι
hi : range f ⊆ range (Sigma.mk i)
⊢ ∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g

Proof state:
case intro.intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
g : α → π i
hf : Continuous (Sigma.mk i ∘ g)
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ ∃ i_1 g_1, Continuous g_1 ∧ Sigma.mk i ∘ g = Sigma.mk i_1 ∘ g_1

Tactic:
refine ⟨i, g, ?_, rfl⟩

Result:
case intro.intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
g : α → π i
hf : Continuous (Sigma.mk i ∘ g)
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ Continuous g

Proof state:
case intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) × π i
hf : Continuous f
i : ι
hi : range f ⊆ range (Sigma.mk i)
⊢ ∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g

Tactic:
rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩

Result:
case intro.intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
g : α → π i
hf : Continuous (Sigma.mk i ∘ g)
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ ∃ i_1 g_1, Continuous g_1 ∧ Sigma.mk i ∘ g = Sigma.mk i_1 ∘ g_1

Proof state:
case intro.intro.intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) × π i
hf : Continuous f
i : ι
s : Set (π i)
hs : range f = Sigma.mk i '' s
⊢ ∃ i, range f ⊆ range (Sigma.mk i)

Tactic:
exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩

Result:
no goals

Proof state:
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) × π i
hf : Continuous f
⊢ ∃ i, range f ⊆ range (Sigma.mk i)

Tactic:
rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩

Result:
case intro.intro.intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) × π i
hf : Continuous f
i : ι
s : Set (π i)
hs : range f = Sigma.mk i '' s
⊢ ∃ i, range f ⊆ range (Sigma.mk i)

Proof state:
case intro.intro
α : Type u
ι : Type u_1
π : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
i : ι
g : α → π i
hf : Continuous (Sigma.mk i ∘ g)
hi : range (Sigma.mk i ∘ g) ⊆ range (Sigma.mk i)
⊢ Continuous g

Tactic:
rwa [← IsEmbedding.sigmaMk.continuous_iff] at hf

Result:
no goals