case intro.intro
H : Type u
H' : Type ?u.44403
M : Type u_1
M' : Type ?u.44409
M'' : Type ?u.44412
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
s : Set M
hsc : Set.Countable s
hsU : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
⊢ SecondCountableTopology M
H : Type u
H' : Type ?u.44403
M : Type u_1
M' : Type ?u.44409
M'' : Type ?u.44412
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
⊢ SecondCountableTopology M
obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ (⋃ (x) (_ : x ∈ s), (chartAt H x).source) = univ :=
  countable_cover_nhds_of_sigma_compact fun x : M ↦ chart_source_mem_nhds H x
no goals
case intro.intro
H : Type u
H' : Type ?u.44403
M : Type u_1
M' : Type ?u.44409
M'' : Type ?u.44412
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
s : Set M
hsc : Set.Countable s
hsU : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
⊢ SecondCountableTopology M
exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc