case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with
  ⟨s, hsc, hsU⟩
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
this : (⋃ (x : α) (_ : x ∈ s), interior (f x)) = univ
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ

case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ (⋃ (x : α) (_ : x ∈ s), interior (f x)) = univ
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ
suffices : (⋃ x ∈ s, interior (f x)) = univ
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ (⋃ (x : α) (_ : x ∈ s), interior (f x)) = univ
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
this : (⋃ (x : α) (_ : x ∈ s), interior (f x)) = univ
⊢ ∃ s, Set.Countable s ∧ (⋃ (x : α) (_ : x ∈ s), f x) = univ

case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ (⋃ (x : α) (_ : x ∈ s), interior (f x)) = univ
exact ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ ∀ (x : α), ∃ i, x ∈ interior (f i)
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ (⋃ (x : α) (_ : x ∈ s), interior (f x)) = univ
simp only [hsU, eq_univ_iff_forall, mem_iUnion]
no goals
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : (⋃ (i : α) (_ : i ∈ s), interior (f i)) = ⋃ (i : α), interior (f i)
⊢ ∀ (x : α), ∃ i, x ∈ interior (f i)
exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩