awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
rwa : interior (closure[inst] (closure[inst] s)) = ∅
rwa₁ rwa₂ rwa₃ rwa₄ : interior (closure[inst] s) = ∅
⊢ IsNowhereDense (closure[inst] s)

Tactic:
rwa [IsNowhereDense, closure_closure]

Premises used: closure_closure, IsNowhereDense
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
⊢ ∃ (t : Set X), s ⊆ t ∧ IsNowhereDense t ∧ IsClosed[inst] t

Tactic:
⟨closure s, subset_closure, ⟨hs.closure, isClosed_closure⟩⟩

Premises used: subset_closure, IsNowhereDense.closure, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsClosed[inst] s ∧ interior s = ∅ ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ
rw₁ : IsClosed[inst] s ∧ interior s = ∅ ↔ IsClosed[inst] s ∧ Dense sᶜ
rw₂ rw₃ : IsClosed[inst] s ∧ Dense sᶜ ↔ IsClosed[inst] s ∧ Dense sᶜ
⊢ IsClosed[inst] s ∧ IsNowhereDense s ↔ IsOpen[inst] sᶜ ∧ Dense sᶜ

Tactic:
rw [and_congr_right IsClosed.isNowhereDense_iff,
    isOpen_compl_iff, interior_eq_empty_iff_dense_compl]

Premises used: and_congr_right, IsClosed.isNowhereDense_iff, interior_eq_empty_iff_dense_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsNowhereDense s ↔ Disjoint s (interior (closure[inst] s))

Tactic:
⟨fun H ↦ H ▸ disjoint_empty _, fun H ↦
    H.closure_left isOpen_interior |>.mono_left interior_subset |>.eq_bot_of_self⟩

Premises used: interior_subset, isOpen_interior, Eq.rec, Disjoint.eq_bot_of_self, Disjoint.mono_left, Iff.intro, Set.disjoint_empty, Disjoint.closure_left, Eq.symm
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsNowhereDense s ↔ ∀ x ∈ s, closure[inst] s ∉ 𝓝 x

Tactic:
simp [isNowhereDense_iff_disjoint, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem,
    mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds, isNowhereDense_iff_disjoint, Set.disjoint_iff_inter_eq_empty, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsNowhereDense s
rw : ∀ (h : ∀ x ∈ s, closure[inst] s ∉ 𝓝 x) ⦃x : X⦄, x ∈ s → closure[inst_1] (f '' s) ∉ 𝓝 (f x)
⊢ IsNowhereDense (f '' s)

Tactic:
rw [isNowhereDense_iff_forall_notMem_nhds, forall_mem_image] at *

Premises used: isNowhereDense_iff_forall_notMem_nhds, Set.forall_mem_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∀ x ∈ s, closure[inst] s ∉ 𝓝 x
⊢ ∀ x ∈ s, f ⁻¹' closure[inst_1] (f '' s) ∉ comap f (𝓝 (f x))

Tactic:
simp_rw [hf.nhds_eq_comap, hf.closure_eq_preimage_closure_image] at h

Premises used: Topology.IsInducing.nhds_eq_comap, Topology.IsInducing.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∀ x ∈ s, f ⁻¹' closure[inst_1] (f '' s) ∉ comap f (𝓝 (f x))
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst_1] (f '' s) ∉ 𝓝 (f x)

Tactic:
fun x x_mem hx ↦ h x x_mem (preimage_mem_comap hx)

Premises used: Filter.preimage_mem_comap, Not
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∀ x ∈ s, f ⁻¹' closure[inst_1] (f '' s) ∉ comap f (𝓝 (f x))
⊢ ∀ ⦃x : X⦄, x ∈ s → closure[inst_1] (f '' s) ∉ 𝓝 (f x)

Tactic:
exact fun x x_mem hx ↦ h x x_mem (preimage_mem_comap hx)

Premises used: Filter.preimage_mem_comap
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Set X
s : Set (↑Y : Type u_1)
hs : IsNowhereDense s
⊢ IsNowhereDense (Subtype.val (p := fun (x : X) ↦ x ∈ Y) '' s)

Tactic:
Topology.IsInducing.subtypeVal.isNowhereDense_image hs

Premises used: Topology.IsInducing.isNowhereDense_image, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : univ ∈ residual X
⊢ IsMeagre.{u_1} (X := X) ∅

Tactic:
rw [IsMeagre, compl_empty]

Premises used: IsMeagre, Set.compl_empty
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ univ ∈ residual X

Tactic:
Filter.univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ univ ∈ residual X

Tactic:
exact Filter.univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hts : t ⊆ s
hs : IsMeagre s
⊢ IsMeagre t

Tactic:
Filter.mem_of_superset hs (compl_subset_compl.mpr hts)

Premises used: Iff.mpr, IsMeagre, Set.compl_subset_compl, Filter.mem_of_superset
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsMeagre s
⊢ IsMeagre (s ∩ t)

Tactic:
hs.mono inter_subset_left

Premises used: Set.inter_subset_left, IsMeagre.mono
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
rw : sᶜ ∩ tᶜ ∈ residual X
⊢ IsMeagre (s ∪ t)

Tactic:
rw [IsMeagre, compl_union]

Premises used: Set.compl_union, IsMeagre
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ sᶜ ∩ tᶜ ∈ residual X

Tactic:
inter_mem hs ht

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsMeagre s
ht : IsMeagre t
⊢ sᶜ ∩ tᶜ ∈ residual X

Tactic:
exact inter_mem hs ht

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
rw : ⋂ (i : ι'), (f i)ᶜ ∈ residual X
⊢ IsMeagre.{u_1} (X := X) (⋃ (i : ι'), f i)

Tactic:
rw [IsMeagre, compl_iUnion]

Premises used: IsMeagre, Set.compl_iUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ ⋂ (i : ι'), (f i)ᶜ ∈ residual X

Tactic:
countable_iInter_mem.mpr hs

Premises used: Iff.mpr, countable_iInter_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hs : ∀ (i : ι'), IsMeagre (f i)
⊢ ⋂ (i : ι'), (f i)ᶜ ∈ residual X

Tactic:
exact countable_iInter_mem.mpr hs

Premises used: Iff.mpr, countable_iInter_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : IsMeagre.{u_1} (X := X) (⋃ (i : (↑I : Type u_3)), f (↑i : ι))
⊢ IsMeagre.{u_1} (X := X) (⋃ i ∈ I, f i)

Tactic:
simpa
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
suffices : IsMeagre.{u_1} (X := X) (⋃ (i : (↑I : Type u_3)), f (↑i : ι))
⊢ IsMeagre.{u_1} (X := X) (⋃ i ∈ I, f i)

Tactic:
suffices IsMeagre (⋃ i : I, f i) by simpa
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
⊢ Countable.{u_3 + 1} (↑I : Type u_3)

Tactic:
have : Countable I := c
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable.{u_3 + 1} (↑I : Type u_3)
hs : ∀ (i : (↑I : Type u_3)), IsMeagre (f (↑i : ι))
⊢ IsMeagre.{u_1} (X := X) (⋃ (i : (↑I : Type u_3)), f (↑i : ι))

Tactic:
apply isMeagre_iUnion

Premises used: isMeagre_iUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable.{u_3 + 1} (↑I : Type u_3)
i : ι
hi : i ∈ I
⊢ IsMeagre (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) : ι))

Tactic:
h i hi
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
f : ι → Set X
h : ∀ i ∈ I, IsMeagre (f i)
this : Countable.{u_3 + 1} (↑I : Type u_3)
i : ι
hi : i ∈ I
⊢ IsMeagre (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) : ι))

Tactic:
exact h i hi
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  (∃ (x : Set (Set X)),
      (∀ t ∈ compl '' x, IsOpen[inst] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ IsMeagre s ↔ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
rw [IsMeagre, mem_residual_iff, compl_bijective.surjective.image_surjective.exists]

Premises used: IsMeagre, Function.Surjective.exists, compl_bijective, Function.Bijective.surjective, Function.Surjective.image_surjective, mem_residual_iff
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw :
  (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ (∃ (x : Set (Set X)),
      (∀ t ∈ compl '' x, IsOpen[inst] t) ∧
        (∀ t ∈ compl '' x, Dense t) ∧ (compl '' x).Countable ∧ ⋂₀ (compl '' x) ⊆ sᶜ) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
simp_rw [← and_assoc, ← forall_and, forall_mem_image, ← isClosed_isNowhereDense_iff_compl,
    sInter_image, ← compl_iUnion₂, compl_subset_compl, ← sUnion_eq_biUnion, and_assoc]

Premises used: isClosed_isNowhereDense_iff_compl, Set.compl_iUnion₂, Set.sUnion_eq_biUnion, Set.compl_subset_compl, and_assoc, Set.sInter_image, Set.forall_mem_image, forall_and
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩

Premises used: Set.sUnion, Exists, HasSubset.Subset, _private.0.isMeagre_iff_countable_union_isNowhereDense.match_7, And, And.right, And.intro, Iff.intro, Exists.intro, Set.Countable
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) →
    ∀ (S : Set (Set X)) (hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x) (hc : (compl '' S).Countable)
      (hsub : s ⊆ ⋃₀ S), S.Countable
refine_2 :
  (∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) →
    ∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
⊢ (∃ (x : Set (Set X)),
      (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
refine_1 : (compl '' compl '' S).Countable
⊢ S.Countable

Tactic:
rw [← compl_compl_image S]

Premises used: Set.compl_compl_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' compl '' S).Countable

Tactic:
hc.image _

Premises used: Set.Countable.image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' compl '' S).Countable

Tactic:
exact hc.image _

Premises used: Set.Countable.image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
h :
  (∀ ⦃x : Set X⦄, x ∈ closure[inst] '' S → IsClosed[inst] x ∧ IsNowhereDense x) ∧
    (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)
⊢ ∃ (x : Set (Set X)),
    (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x

Tactic:
use closure '' S

Premises used: closure
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
h :
  (∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] (closure[inst] x) ∧ IsNowhereDense (closure[inst] x)) ∧
    (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)
⊢ (∀ ⦃x : Set X⦄, x ∈ closure[inst] '' S → IsClosed[inst] x ∧ IsNowhereDense x) ∧
    (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)

Tactic:
rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] (closure[inst] x) ∧ IsNowhereDense (closure[inst] x)) ∧
    (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)

Tactic:
⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩,
      (hc.image _).image _, hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩

Premises used: subset_closure, IsNowhereDense.closure, HasSubset.Subset.trans, Set.Countable.image, Set.sUnion_mono_subsets, And.intro, isClosed_closure
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
S : Set (Set X)
hS : ∀ t ∈ S, IsNowhereDense t
hc : S.Countable
hsub : s ⊆ ⋃₀ S
⊢ (∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst] (closure[inst] x) ∧ IsNowhereDense (closure[inst] x)) ∧
    (compl '' closure[inst] '' S).Countable ∧ s ⊆ ⋃₀ (closure[inst] '' S)

Tactic:
exact ⟨fun s hs ↦ ⟨isClosed_closure, (hS s hs).closure⟩,
      (hc.image _).image _, hsub.trans (sUnion_mono_subsets fun s ↦ subset_closure)⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : ¬IsMeagre s
contrapose! : ∀ (hs : s = ∅), IsMeagre s
⊢ s.Nonempty

Tactic:
contrapose! hs
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : s = ∅
⊢ IsMeagre s

Tactic:
simpa [hs] using IsMeagre.empty

Premises used: IsMeagre.empty
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsNowhereDense s
rw : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ IsMeagre s

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense]

Premises used: isMeagre_iff_countable_union_isNowhereDense
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ ∀ (t : Set X), Membership.mem (γ := Set (Set X)) {s} t → IsNowhereDense t

Tactic:
simpa
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ Set.Countable (α := Set X) {s}

Tactic:
simp
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ s ⊆ ⋃₀ {s}

Tactic:
simp
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
exact ⟨{s}, by simpa, by simp, by simp⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ¬IsMeagre.{u_1} (X := X) (⋃ i ∈ I, A i)
contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ I), IsMeagre (A i)), IsMeagre.{u_1} (X := X) (⋃ i ∈ I, A i)
⊢ ∃ i ∈ I, ¬IsMeagre (A i)

Tactic:
contrapose! h
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ∀ (i : ι) (_ : i ∈ I), IsMeagre (A i)
⊢ IsMeagre.{u_1} (X := X) (⋃ i ∈ I, A i)

Tactic:
isMeagre_biUnion c h

Premises used: isMeagre_biUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
c : I.Countable
A : ι → Set X
h : ∀ (i : ι) (_ : i ∈ I), IsMeagre (A i)
⊢ IsMeagre.{u_1} (X := X) (⋃ i ∈ I, A i)

Tactic:
exact isMeagre_biUnion c h

Premises used: isMeagre_biUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsMeagre s
rw :
  ∀ (h : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S),
    ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
⊢ IsMeagre (f '' s)

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense] at *

Premises used: isMeagre_iff_countable_union_isNowhereDense
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
obtain :
  ∀ (T : Set (Set X)) (isNowhereDense : ∀ t ∈ T, IsNowhereDense t) (countable : T.Countable) (cover : s ⊆ ⋃₀ T),
    ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
⊢ ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S

Tactic:
obtain ⟨T, isNowhereDense, countable, cover⟩ := h

Premises used: Encodable.countable
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S

Tactic:
⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
refine : ∀ t ∈ image f '' T, IsNowhereDense t
refine₁ : f '' s ⊆ ⋃₀ (image f '' T)
⊢ ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S

Tactic:
refine ⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
this : ∀ (t : Set X) (tT : t ∈ T) (tu : f '' t = u), IsNowhereDense u
⊢ u ∈ image f '' T → IsNowhereDense u

Tactic:
⟨t, tT, tu⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
t : Set X
tT : t ∈ T
tu : f '' t = u
rw : IsNowhereDense (f '' t)
⊢ IsNowhereDense u

Tactic:
rw [← tu]
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
t : Set X
tT : t ∈ T
tu : f '' t = u
⊢ IsNowhereDense (f '' t)

Tactic:
apply hf.isNowhereDense_image (isNowhereDense t tT)

Premises used: Topology.IsInducing.isNowhereDense_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

Tactic:
case isNowhereDense =>
    intro u ⟨t, tT, tu⟩
    rw [← tu]
    apply hf.isNowhereDense_image (isNowhereDense t tT)
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
rw : f '' s ⊆ f '' ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)

Tactic:
rw [← Set.image_sUnion]

Premises used: Set.image_sUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
grw grw₁ : f '' ⋃₀ T ⊆ f '' ⋃₀ T
⊢ f '' s ⊆ f '' ⋃₀ T

Tactic:
grw [cover]
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
case case₁ case₂ : f '' s ⊆ f '' ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)

Tactic:
case cover =>
    rw [← Set.image_sUnion]
    grw [cover]

Premises used: Set.image_sUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
m : Set (↑s : Type u_1)
h : IsMeagre m
⊢ IsMeagre (Subtype.val (p := fun (x : X) ↦ x ∈ s) '' m)

Tactic:
Topology.IsInducing.subtypeVal.isMeagre_image h

Premises used: Topology.IsInducing.isMeagre_image, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
⊢ NormalSpace X

Tactic:
(@UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity X
    (pseudoMetrizableSpaceUniformity X)
    (pseudoMetrizableSpaceUniformity_countably_generated X)).toNormalSpace

Premises used: CompletelyNormalSpace.toNormalSpace
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this : UniformSpace X := pseudoMetrizableSpaceUniformity X
⊢ (uniformity X).IsCountablyGenerated

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated X
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (uniformity X).IsCountablyGenerated
rcases :
  ∀ (U : ℕ → SetRel X X) (hUo : ∀ (i : ℕ), U i ∈ uniformity X ∧ IsOpen (U i))
    (hU : (uniformity X).HasBasis (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦ id (U i)), IsGδ s
⊢ IsGδ s

Tactic:
rcases (@uniformity_hasBasis_open X _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩

Premises used: Filter.HasBasis.exists_antitone_subbasis, uniformity_hasBasis_open