awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
rw : Dense (⋂₀ (f '' S))
⊢ Dense.{u_1} (X := X) (⋂ s ∈ S, f s)

Tactic:
rw [← sInter_image]

Premises used: Set.sInter_image
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense (⋂₀ (f '' S))

Tactic:
dense_sInter_of_isOpen ?_ (hS.image _) ?_

Premises used: Set.Countable.image, dense_sInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
refine_1 : ∀ s ∈ f '' S, IsOpen[inst] s
refine_2 : ∀ s ∈ f '' S, Dense s
⊢ Dense (⋂₀ (f '' S))

Tactic:
refine dense_sInter_of_isOpen ?_ (hS.image _) ?_

Premises used: Set.Countable.image, dense_sInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ ⦃x : α⦄, x ∈ S → IsOpen[inst] (f x)
⊢ ∀ s ∈ f '' S, IsOpen[inst] s

Tactic:
rwa [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst] (f s)
hS : S.Countable
hd refine_2 refine_2₁ refine_2₂ refine_2₃ : ∀ ⦃x : α⦄, x ∈ S → Dense (f x)
⊢ ∀ s ∈ f '' S, Dense s

Tactic:
rwa [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
f : ι → Set X
ho : ∀ (i : ι), IsOpen[inst] (f i)
hd : ∀ (i : ι), Dense (f i)
⊢ Dense.{u_1} (X := X) (⋂ (s : ι), f s)

Tactic:
dense_sInter_of_isOpen (forall_mem_range.2 ho) (countable_range _) (forall_mem_range.2 hd)

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, Set.countable_range, dense_sInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
mp : s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t
mpr : (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X
⊢ s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
constructor
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
mp :
  (∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s) →
    ∃ t ⊆ s, IsGδ t ∧ Dense t
⊢ s ∈ residual X → ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
rw [mem_residual_iff]

Premises used: mem_residual_iff
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
mp : Dense (⋂₀ S)
⊢ ∃ t ⊆ s, IsGδ t ∧ Dense t

Tactic:
refine ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, ?_⟩
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)

Tactic:
dense_sInter_of_isOpen hSo Sct hSd

Premises used: dense_sInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
S : Set (Set X)
hSo : ∀ t ∈ S, IsOpen[inst] t
hSd : ∀ t ∈ S, Dense t
Sct : S.Countable
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)

Tactic:
exact dense_sInter_of_isOpen hSo Sct hSd

Premises used: dense_sInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s t : Set X
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual X

Tactic:
mem_of_superset (residual_of_dense_Gδ ho hd) ts

Premises used: residual_of_dense_Gδ, Filter.mem_of_superset
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s t : Set X
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual X

Tactic:
exact mem_of_superset (residual_of_dense_Gδ ho hd) ts

Premises used: residual_of_dense_Gδ, Filter.mem_of_superset
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
simp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
⊢ (∀ᶠ (x : X) in residual X, p x) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x

Tactic:
simp only [Filter.Eventually, mem_residual, subset_def, mem_setOf_eq]

Premises used: Set.subset_def, Filter.Eventually, Set.mem_setOf_eq, mem_residual
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
p : X → Prop
mp : (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr : (∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₁ mp₂ mp₃ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₁ mpr₂ mpr₃ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₄ mp₅ mp₆ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mpr₄ mpr₅ mpr₆ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mp₇ mp₈ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
mp₉ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
mp₁₀ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
mp₁₁ : ∀ (w : Set X), (∀ x ∈ w, p x) → IsGδ w → Dense w → IsGδ w ∧ Dense w ∧ ∀ x ∈ w, p x
mp₁₂ : (w : Set X) → (∀ x ∈ w, p x) → IsGδ w → Dense w → Set X
mpr₇ mpr₈ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → ∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t
mpr₉ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → (∀ x ∈ w, p x) ∧ IsGδ w ∧ Dense w
mpr₁₀ : (w : Set X) → IsGδ w → Dense w → (∀ x ∈ w, p x) → Set X
mpr₁₁ : ∀ (w : Set X), IsGδ w → Dense w → (∀ x ∈ w, p x) → (∀ x ∈ w, p x) ∧ IsGδ w ∧ Dense w
mpr₁₂ : (w : Set X) → IsGδ w → Dense w → (∀ x ∈ w, p x) → Set X
⊢ (∃ (t : Set X), (∀ x ∈ t, p x) ∧ IsGδ t ∧ Dense t) ↔ ∃ (t : Set X), IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x

Tactic:
tauto
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hs : s ∈ residual X
⊢ Dense s

Tactic:
let ⟨_, hts, _, hd⟩ := mem_residual.1 hs
  hd.mono hts

Premises used: Dense, Dense.mono, _private.0.dense_of_mem_residual.match_1, mem_residual, Iff.mp
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hs : IsOpen[inst] s
hne : s.Nonempty
h : IsMeagre s
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : sᶜ ∈ residual X), sᶜ ∈ residual X
⊢ sᶜ ∈ residual X

Tactic:
rwa [IsMeagre] at h

Premises used: IsMeagre
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hs : IsOpen[inst] s
hne : s.Nonempty
h : IsMeagre s
obtain : ∀ (x : X) (hx : x ∈ s) (hxc : x ∈ sᶜ), False
⊢ False

Tactic:
obtain ⟨x, hx, hxc⟩ :=
    (dense_of_mem_residual (by rwa [IsMeagre] at h)).inter_open_nonempty s hs hne

Premises used: dense_of_mem_residual, Dense.inter_open_nonempty
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hs : IsOpen[inst] s
hne : s.Nonempty
h : IsMeagre s
x : X
hx : x ∈ s
hxc : x ∈ sᶜ
⊢ False

Tactic:
hxc hx
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hs : IsOpen[inst] s
hne : s.Nonempty
h : IsMeagre s
x : X
hx : x ∈ s
hxc : x ∈ sᶜ
⊢ False

Tactic:
exact hxc hx
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsGδ s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
⊢ Dense (⋂₀ S)

Tactic:
dense_of_mem_residual ((countable_sInter_mem hS).mpr
    (fun _ hs => residual_of_dense_Gδ (ho _ hs) (hd _ hs)))

Premises used: Iff.mpr, dense_of_mem_residual, residual_of_dense_Gδ, countable_sInter_mem
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
f : ι → Set X
ho : ∀ (s : ι), IsGδ (f s)
hd : ∀ (s : ι), Dense (f s)
⊢ Dense.{u_1} (X := X) (⋂ (s : ι), f s)

Tactic:
dense_sInter_of_Gδ (forall_mem_range.2 ‹_›) (countable_range _) (forall_mem_range.2 ‹_›)

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, Set.countable_range, dense_sInter_of_Gδ
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
rw : Dense.{u_1} (X := X) (⋂ (x : (↑S : Type u_2)), f (↑x : α) ⋯)
⊢ Dense.{u_1} (X := X) (⋂ (s : α), ⋂ (h : s ∈ S), f s h)

Tactic:
rw [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
⊢ Countable.{u_2 + 1} (↑S : Type u_2)

Tactic:
haveI := hS.to_subtype
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
this : Countable.{u_2 + 1} (↑S : Type u_2)
⊢ Dense.{u_1} (X := X) (⋂ (x : (↑S : Type u_2)), f (↑x : α) ⋯)

Tactic:
dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2

Premises used: dense_iInter_of_Gδ, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
this : Countable.{u_2 + 1} (↑S : Type u_2)
⊢ Dense.{u_1} (X := X) (⋂ (x : (↑S : Type u_2)), f (↑x : α) ⋯)

Tactic:
exact dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
rw : Dense.{u_1} (X := X) (⋂ (b : Bool), bif b then s else t)
⊢ Dense (s ∩ t)

Tactic:
rw [inter_eq_iInter]

Premises used: Set.inter_eq_iInter
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
ho : ∀ (s_1 : Bool), IsGδ (bif s_1 then s else t)
hd : ∀ (s_1 : Bool), Dense (bif s_1 then s else t)
⊢ Dense.{u_1} (X := X) (⋂ (b : Bool), bif b then s else t)

Tactic:
apply dense_iInter_of_Gδ

Premises used: dense_iInter_of_Gδ
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), IsGδ (bif s_1 then s else t)

Tactic:
simp [Bool.forall_bool, *]

Premises used: Bool.forall_bool
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ ∀ (s_1 : Bool), Dense (bif s_1 then s else t)

Tactic:
simp [Bool.forall_bool, *]

Premises used: Bool.forall_bool
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
⊢ ∀ (i : ι), IsOpen[inst] (g i)

Tactic:
have hgo : ∀ i, IsOpen (g i) := fun i => isClosed_frontier.isOpen_compl
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
⊢ Dense.{u_1} (X := X) (⋂ (i : ι), g i)

Tactic:
dense_iInter_of_isOpen hgo fun i x => ?_

Premises used: dense_iInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
refine : ∀ (i : ι) (x : X), x ∈ closure[inst] (g i)
⊢ Dense.{u_1} (X := X) (⋂ (i : ι), g i)

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

Premises used: dense_iInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
i : ι
x : X
rw : Membership.mem (γ := Set X) ∅ᶜ x
⊢ x ∈ closure[inst] (g i)

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

Premises used: interior_frontier, closure_compl
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
i : ι
x : X
⊢ Membership.mem (γ := Set X) ∅ᶜ x

Tactic:
id

Premises used: Set.Mem, setOf, id, Not
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
i : ι
x : X
⊢ Membership.mem (γ := Set X) ∅ᶜ x

Tactic:
exact id

Premises used: id
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
⊢ Dense.{u_1} (X := X) (⋂ (i : ι), g 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
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
hgd : Dense.{u_1} (X := X) (⋂ (i : ι), g i)
⊢ Dense.{u_1} (X := X) (⋃ (i : ι), interior (f i))

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

Premises used: Dense.mono, Dense.inter_of_Gδ, IsGδ.iInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
hgd : Dense.{u_1} (X := X) (⋂ (i : ι), g i)
refine : s ∩ ⋂ (i : ι), g i ⊆ ⋃ (i : ι), interior (f i)
⊢ Dense.{u_1} (X := X) (⋃ (i : ι), interior (f i))

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

Premises used: Dense.mono, Dense.inter_of_Gδ, IsGδ.iInter_of_isOpen
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
hgd : Dense.{u_1} (X := X) (⋂ (i : ι), g i)
x : X
hxs : x ∈ s
hxg : Membership.mem (γ := Set X) (⋂ (i : ι), g i) x
⊢ ∀ (i : ι), x ∈ g i

Tactic:
rw [mem_iInter] at hxg

Premises used: Set.mem_iInter
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
hgd : Dense.{u_1} (X := X) (⋂ (i : ι), g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
rcases : ∀ (i : ι) (hi : x ∈ f i), Membership.mem (γ := Set X) (⋃ (i : ι), interior (f i)) x
⊢ Membership.mem (γ := Set X) (⋃ (i : ι), interior (f i)) x

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

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
hgd : Dense.{u_1} (X := X) (⋂ (i : ι), g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ Membership.mem (γ := Set X) (⋃ (i : ι), interior (f i)) x

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

Premises used: Iff.mpr, self_diff_frontier, Set.mem_iUnion, Eq.rec, And.intro, Exists.intro
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : (i : ι) → Set X := fun (i : ι) ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst] (g i)
hgd : Dense.{u_1} (X := X) (⋂ (i : ι), g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ Membership.mem (γ := Set X) (⋃ (i : ι), interior (f i)) x

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

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
hc : ∀ i ∈ t, IsClosed[inst] (f i)
hU : s ⊆ ⋃ i ∈ t, f i
⊢ Countable.{u_2 + 1} (↑t : Type u_2)

Tactic:
haveI := ht.to_subtype
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
hc : ∀ i ∈ t, IsClosed[inst] (f i)
hU : s ⊆ ⋃ i ∈ t, f i
this : Countable.{u_2 + 1} (↑t : Type u_2)
simp :
  ∀ (hc : ∀ (x : (↑t : Type u_2)), IsClosed[inst] (f (↑x : α))) (hU : s ⊆ ⋃ (x : (↑t : Type u_2)), f (↑x : α)),
    Dense.{u_1} (X := X) (⋃ (x : (↑t : Type u_2)), interior (f (↑x : α)))
⊢ Dense.{u_1} (X := X) (⋃ i ∈ t, interior (f i))

Tactic:
simp only [biUnion_eq_iUnion, SetCoe.forall'] at *

Premises used: Set.biUnion_eq_iUnion, SetCoe.forall'
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
this : Countable.{u_2 + 1} (↑t : Type u_2)
hc : ∀ (x : (↑t : Type u_2)), IsClosed[inst] (f (↑x : α))
hU : s ⊆ ⋃ (x : (↑t : Type u_2)), f (↑x : α)
⊢ Dense.{u_1} (X := X) (⋃ (x : (↑t : Type u_2)), interior (f (↑x : α)))

Tactic:
hs.dense_iUnion_interior_of_closed hd hc hU

Premises used: IsGδ.dense_iUnion_interior_of_closed
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
t : Set α
s : Set X
hs : IsGδ s
hd : Dense s
ht : t.Countable
f : α → Set X
this : Countable.{u_2 + 1} (↑t : Type u_2)
hc : ∀ (x : (↑t : Type u_2)), IsClosed[inst] (f (↑x : α))
hU : s ⊆ ⋃ (x : (↑t : Type u_2)), f (↑x : α)
⊢ Dense.{u_1} (X := X) (⋃ (x : (↑t : Type u_2)), interior (f (↑x : α)))

Tactic:
exact hs.dense_iUnion_interior_of_closed hd hc hU

Premises used: IsGδ.dense_iUnion_interior_of_closed
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
T : Set (Set X)
s : Set X
hs : IsGδ s
hd : Dense s
hc : T.Countable
hc' : ∀ t ∈ T, IsClosed[inst] t
hU rwa rwa₁ rwa₂ rwa₃ : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃ i ∈ T, i

Tactic:
rwa [← sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
α : Type u_2
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set α
f : α → Set X
hc : ∀ s ∈ S, IsClosed[inst] (f s)
hS : S.Countable
hU : Eq.{u_1 + 1} (α := Set X) (⋃ s ∈ S, f s) univ
⊢ Dense.{u_1} (X := X) (⋃ s ∈ S, interior (f s))

Tactic:
IsGδ.univ.dense_biUnion_interior_of_closed dense_univ hS hc hU.ge

Premises used: Eq.ge, dense_univ, IsGδ.dense_biUnion_interior_of_closed, IsGδ.univ
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
S : Set (Set X)
hc : ∀ s ∈ S, IsClosed[inst] s
hS : S.Countable
hU : ⋃₀ S = univ
⊢ Dense.{u_1} (X := X) (⋃ s ∈ S, interior s)

Tactic:
IsGδ.univ.dense_sUnion_interior_of_closed dense_univ hS hc hU.ge

Premises used: IsGδ.dense_sUnion_interior_of_closed, Eq.ge, dense_univ, IsGδ.univ
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Countable ι
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), f i) univ
⊢ Dense.{u_1} (X := X) (⋃ (i : ι), interior (f i))

Tactic:
IsGδ.univ.dense_iUnion_interior_of_closed dense_univ hc hU.ge

Premises used: Eq.ge, dense_univ, IsGδ.univ, IsGδ.dense_iUnion_interior_of_closed
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
ι : Sort u_3
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
inst_3 : Countable ι
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst] (f i)
hU : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ι), f i) univ
⊢ ∃ (i : ι), (interior (f i)).Nonempty

Tactic:
simpa using (dense_iUnion_interior_of_closed hc hU).nonempty

Premises used: dense_iUnion_interior_of_closed, Dense.nonempty
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
rcases : ∀ (t : Set X) (hts : t ⊆ sᶜ) (htG : IsGδ t) (hd' : Dense t), False
⊢ False

Tactic:
rcases mem_residual.1 h with ⟨t, hts, htG, hd'⟩

Premises used: mem_residual, Iff.mp
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
inst_2 : Nonempty X
s : Set X
hs : IsGδ s
hd : Dense s
h : IsMeagre s
t : Set X
hts : t ⊆ sᶜ
htG : IsGδ t
hd' : Dense t
rcases : ∀ (x : X) (hx₁ : x ∈ s) (hx₂ : x ∈ t), False
⊢ False

Tactic:
rcases (hd.inter_of_Gδ hs htG hd').nonempty with ⟨x, hx₁, hx₂⟩

Premises used: Dense.nonempty, Dense.inter_of_Gδ