awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
baire_property :
  ∀ (g : (n : ℕ) → Set X) (hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)) (hg2 : ∀ (n : ℕ), Dense (g n))
    (hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n),
    Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)

Tactic:
choose g hg1 hg2 hg3 using fun n => exists_open_dense_of_open_dense_subtype hd (hof n) (hdf n)

Premises used: exists_open_dense_of_open_dense_subtype
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
n : ℕ
⊢ s ⊆ V n

Tactic:
simp [hV.2, iInter_subset]

Premises used: And.right, Set.iInter_subset
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)

Tactic:
have h_inter_dense : Dense (⋂ n, g n ∩ V n) := BaireSpace.baire_property (fun n ↦ g n ∩ V n)
    (fun n => (hg1 n).inter (hV.1 n))
    (fun n => (hg2 n).inter_of_isOpen_left (hd.mono (by simp [hV.2, iInter_subset])) (hg1 n))
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
h :
  ∀ (x : X),
    Membership.mem (γ := Set X) (⋂ (n : ℕ), g n ∩ V n) x ↔
      Membership.mem (γ := Set X)
        (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n)) x
⊢ Eq.{u_1 + 1} (α := Set X) (⋂ (n : ℕ), g n ∩ V n)
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n))

Tactic:
ext
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
x : X
h :
  ∀ (hG : IsGδ.{u_1} (X := X) (⋂ (n : ℕ), V n)) (hd : Dense.{u_1} (X := X) (⋂ (n : ℕ), V n))
    (hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)) (hdf : ∀ (n : ℕ), Dense (f n))
    (hV_1 : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n) (hg1 : ∀ (n : ℕ), IsOpen[inst] (g n))
    (hg2 : ∀ (n : ℕ), Dense (g n)) (hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n)
    (h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)),
    (∀ (i : ℕ), x ∈ g i ∧ x ∈ V i) ↔
      ∃ (x_1 : ∀ (i : ℕ), x ∈ V i), ∀ (i : ℕ), Subtype.mk (p := fun (a : X) ↦ a ∈ s) x ⋯ ∈ f i
⊢ Membership.mem (γ := Set X) (⋂ (n : ℕ), g n ∩ V n) x ↔
    Membership.mem (γ := Set X)
      (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n)) x

Tactic:
simp_all
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
f : ℕ → Set (↑s : Type u_1)
V : ℕ → Set X
hV_1 : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
x : X
hG : IsGδ.{u_1} (X := X) (⋂ (n : ℕ), V n)
hd : Dense.{u_1} (X := X) (⋂ (n : ℕ), V n)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
⊢ (∀ (i : ℕ), x ∈ g i ∧ x ∈ V i) ↔
    ∃ (x_1 : ∀ (i : ℕ), x ∈ V i), ∀ (i : ℕ), Subtype.mk (p := fun (a : X) ↦ a ∈ s) x ⋯ ∈ f i

Tactic:
grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
⊢ Eq.{u_1 + 1} (α := Set X) (⋂ (n : ℕ), g n ∩ V n)
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n))

Tactic:
have h_inter_eq : ⋂ n, g n ∩ V n = ⋂ n, f n := by ext; simp_all; grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set X) (⋂ (n : ℕ), g n ∩ V n)
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n))
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)

Tactic:
Subtype.dense_iff.mpr fun a _ ↦ h_inter_eq ▸ h_inter_dense a

Premises used: Iff.mpr, Subtype.dense_iff, Eq.rec
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
V : ℕ → Set X
hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n
g : (n : ℕ) → Set X
hg1 : ∀ (n : ℕ), IsOpen[inst] (g n)
hg2 : ∀ (n : ℕ), Dense (g n)
hg3 : ∀ (n : ℕ), Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' g n = f n
h_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), g n ∩ V n)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set X) (⋂ (n : ℕ), g n ∩ V n)
    (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (⋂ (n : ℕ), f n))
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)

Tactic:
exact Subtype.dense_iff.mpr fun a _ ↦ h_inter_eq ▸ h_inter_dense a

Premises used: Iff.mpr, Subtype.dense_iff
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
baire_property :
  ∀ (f : ℕ → Set Y),
    (∀ (n : ℕ), IsOpen[inst_2] (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)
⊢ BaireSpace Y

Tactic:
constructor
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
⊢ ∀ (n : ℕ), IsOpen[inst] (c n)

Tactic:
have c_open (n : ℕ) : IsOpen (c n) := IsOpen.union (hp.isOpenMap (f n) (hof n))
    isClosed_closure.isOpen_compl
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
rw : closure[inst] (c n) ⊆ univ ∧ univ ⊆ closure[inst] (c n)
⊢ Dense (c n)

Tactic:
rw [dense_iff_closure_eq, subset_antisymm_iff]

Premises used: dense_iff_closure_eq, subset_antisymm_iff
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ univ ⊆ interior (closure[inst] s) ∪ (interior (closure[inst] s))ᶜ

Tactic:
grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
h₁ : interior (closure[inst] s) ⊆ closure[inst] s
⊢ interior (closure[inst] s) ∪ (interior (closure[inst] s))ᶜ ⊆ closure[inst] s ∪ (interior (closure[inst] s))ᶜ

Tactic:
gcongr
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ interior (closure[inst] s) ⊆ closure[inst] s

Tactic:
interior_subset

Premises used: interior_subset
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ interior (closure[inst] s) ⊆ closure[inst] s

Tactic:
exact interior_subset

Premises used: interior_subset
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ closure[inst] (p '' f n) ⊆ closure[inst] (p '' f n)

Tactic:
simp
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ (interior (closure[inst] s))ᶜ ⊆ closure[inst] (closure[inst] s)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
⊢ univ ⊆ closure[inst] (c n)

Tactic:
have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
n : ℕ
this : univ ⊆ closure[inst] (c n)
⊢ closure[inst] (c n) ⊆ univ ∧ univ ⊆ closure[inst] (c n)

Tactic:
grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
⊢ ∀ (n : ℕ), Dense (c n)

Tactic:
have c_dense (n : ℕ) : Dense (c n) := by
    rw [dense_iff_closure_eq, subset_antisymm_iff]
    have : univ ⊆ closure (c n) := calc
      _ ⊆ (interior (closure s)) ∪ (interior (closure s))ᶜ := by grind
      _ ⊆ closure s ∪ (interior (closure s))ᶜ := by gcongr; exact interior_subset
      _ ⊆ closure (p '' f n) ∪ (interior (closure s))ᶜ := union_subset_union
          (closure_minimal (hp.continuous.range_subset_closure_image_dense (hdf n))
          isClosed_closure) (subset_refl (interior (closure s))ᶜ)
      _ ⊆ closure (p '' f n) ∪ closure ((closure s)ᶜ) := union_subset_union (by simp) (by simp)
      _ = closure (c n) := closure_union.symm
    grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)

Tactic:
have c_inter_dense : Dense (⋂ n, c n) := dense_iInter_of_isOpen_nat c_open c_dense
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
h : ∀ (x : Y), Membership.mem (γ := Set Y) (⋂ (n : ℕ), f n) x ↔ x ∈ p ⁻¹' ⋂ (n : ℕ), c n
⊢ ⋂ (n : ℕ), f n = p ⁻¹' ⋂ (n : ℕ), c n

Tactic:
ext x
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
h : (∀ (i : ℕ), x ∈ f i) ↔ ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s
⊢ Membership.mem (γ := Set Y) (⋂ (n : ℕ), f n) x ↔ x ∈ p ⁻¹' ⋂ (n : ℕ), c n

Tactic:
simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]

Premises used: Set.mem_union, Set.mem_iInter, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
h : ∀ (i : ℕ), x ∈ f i
i : ℕ
⊢ p x ∈ p '' f i ∨ p x ∉ closure[inst] s

Tactic:
grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
h : ∀ (h : ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s) (i : ℕ), x ∈ f i
⊢ (∀ (i : ℕ), x ∈ f i) ↔ ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s

Tactic:
refine ⟨fun h i => by grind, fun h i => ?_⟩
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
h : ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s
i : ℕ
⊢ x ∈ f i

Tactic:
hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
      (subset_closure (mem_range_self x)))

Premises used: Set.mem_range_self, Iff.mpr, Topology.IsOpenEmbedding.toIsEmbedding, subset_closure, Topology.IsEmbedding.injective, Iff.mp, imp_iff_or_not, Function.Injective.mem_set_image
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
x : Y
h : ∀ (i : ℕ), p x ∈ p '' f i ∨ p x ∉ closure[inst] s
i : ℕ
⊢ x ∈ f i

Tactic:
exact hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
      (subset_closure (mem_range_self x)))

Premises used: Set.mem_range_self, Iff.mpr, Topology.IsOpenEmbedding.toIsEmbedding, subset_closure, Topology.IsEmbedding.injective, Iff.mp, imp_iff_or_not, Function.Injective.mem_set_image
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
⊢ ⋂ (n : ℕ), f n = p ⁻¹' ⋂ (n : ℕ), c n

Tactic:
have c_inter_eq : ⋂ n, f n = p ⁻¹' (⋂ n, c n) := by
    ext x
    simp only [mem_iInter, mem_preimage, mem_union, mem_compl_iff, c]
    refine ⟨fun h i => by grind, fun h i => ?_⟩
    exact hp.injective.mem_set_image.mp (imp_iff_or_not.mpr (h i)
      (subset_closure (mem_range_self x)))
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
c_inter_eq : ⋂ (n : ℕ), f n = p ⁻¹' ⋂ (n : ℕ), c n
⊢ Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)

Tactic:
c_inter_eq ▸ Dense.preimage c_inter_dense hp.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, Eq.rec, Eq.symm, Dense.preimage
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
Y : Type u_4
inst_2 : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst_2] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : (n : ℕ) → Set X := fun (n : ℕ) ↦ p '' f n ∪ (closure[inst] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense.{u_1} (X := X) (⋂ (n : ℕ), c n)
c_inter_eq : ⋂ (n : ℕ), f n = p ⁻¹' ⋂ (n : ℕ), c n
⊢ Dense.{u_4} (X := Y) (⋂ (n : ℕ), f n)

Tactic:
exact c_inter_eq ▸ Dense.preimage c_inter_dense hp.isOpenMap
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hO : IsOpen[inst] s
⊢ BaireSpace.{u_1} (↑s : Type u_1)

Tactic:
hO.isOpenEmbedding_subtypeVal.baireSpace

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.baireSpace
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
inl : ∀ (h : S = ∅), Dense (⋂₀ S)
inr : ∀ (h : S.Nonempty), Dense (⋂₀ S)
⊢ Dense (⋂₀ S)

Tactic:
rcases S.eq_empty_or_nonempty with h | h

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S = ∅
⊢ Dense (⋂₀ S)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen[inst] s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S.Nonempty
inr :
  ∀ (f : ℕ → Set X) (ho : ∀ s ∈ range f, IsOpen[inst] s) (hS : (range f).Countable) (hd : ∀ s ∈ range f, Dense s)
    (h : (range f).Nonempty), Dense (⋂₀ range f)
⊢ Dense (⋂₀ S)

Tactic:
rcases hS.exists_eq_range h with ⟨f, rfl⟩

Premises used: Set.Countable.exists_eq_range, rfl
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
f : ℕ → Set X
ho : ∀ s ∈ range f, IsOpen[inst] s
hS : (range f).Countable
hd : ∀ s ∈ range f, Dense s
h : (range f).Nonempty
⊢ Dense (⋂₀ range f)

Tactic:
dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)

Premises used: iInf, Set.forall_mem_range, Set.Mem, setOf, Iff.mp, dense_iInter_of_isOpen_nat, Set.sInter
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
f : ℕ → Set X
ho : ∀ s ∈ range f, IsOpen[inst] s
hS : (range f).Countable
hd : ∀ s ∈ range f, Dense s
h : (range f).Nonempty
⊢ Dense (⋂₀ range f)

Tactic:
exact dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)

Premises used: Set.forall_mem_range, Iff.mp, dense_iInter_of_isOpen_nat