-- Mathlib/Topology/Baire/Lemmas.lean
theorem IsGδ.dense_iUnion_interior_of_closed [Countable ι] {s : Set X} (hs : IsGδ s) (hd : Dense s)
    {f : ι → Set X} (hc : ∀ i, IsClosed (f i)) (hU : s ⊆ ⋃ i, f i) :
    Dense (⋃ i, interior (f i))

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : X
⊢ x ∈ closure (g i)

Tactic:
rw [closure_compl, interior_frontier (hc _)]

Result:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : X
⊢ x ∈ ∅ᶜ

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : X
⊢ x ∈ ∅ᶜ

Tactic:
exact id

Result:
no goals

Proof state:
case intro
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : x ∈ ⋂ i, g i
⊢ x ∈ ⋃ i, interior (f i)

Tactic:
rw [mem_iInter] at hxg

Result:
case intro
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ i, interior (f i)

Proof state:
case intro.intro
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ i, interior (f i)

Tactic:
exact mem_iUnion.2 ⟨i, self_diff_frontier (f i) ▸ ⟨hi, hxg _⟩⟩

Result:
no goals

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
⊢ s ∩ ⋂ i, g i ⊆ ⋃ i, interior (f i)

Tactic:
rintro x ⟨hxs, hxg⟩

Result:
case intro
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : x ∈ ⋂ i, g i
⊢ x ∈ ⋃ i, interior (f i)

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
⊢ Dense (⋃ i, interior (f i))

Tactic:
have hgo : ∀ i, IsOpen (g i) := fun i => isClosed_frontier.isOpen_compl

Result:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋃ i, interior (f i))

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋃ i, interior (f i))

Tactic:
have hgd : Dense (⋂ i, g i) := by
  refine dense_iInter_of_isOpen hgo fun i x => ?_
  rw [closure_compl, interior_frontier (hc _)]
  exact id

Result:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
⊢ Dense (⋃ i, interior (f i))

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋂ i, g i)

Tactic:
refine dense_iInter_of_isOpen hgo fun i x => ?_

Result:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : X
⊢ x ∈ closure (g i)

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
⊢ Dense (⋃ i, interior (f i))

Tactic:
refine (hd.inter_of_Gδ hs (.iInter_of_isOpen fun i => (hgo i)) hgd).mono ?_

Result:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
⊢ s ∩ ⋂ i, g i ⊆ ⋃ i, interior (f i)

Proof state:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
⊢ Dense (⋃ i, interior (f i))

Tactic:
let g i := (frontier (f i))ᶜ

Result:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
⊢ Dense (⋃ i, interior (f i))

Proof state:
case intro
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ i, interior (f i)

Tactic:
rcases mem_iUnion.1 (hU hxs) with ⟨i, hi⟩

Result:
case intro.intro
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i => (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ i, interior (f i)