awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Filter
Goal:
α : Type u_2
X : Type u_4
inst : TopologicalSpace X
f : α → X
l : Filter α
x : X
h : Tendsto f l (𝓝 x)
⊢ Tendsto (𝓝 ∘ f) l (𝓝 (𝓝 x))

Tactic:
(continuous_nhds.tendsto _).comp h

Premises used: Continuous.tendsto, Filter.Tendsto.comp, Filter.continuous_nhds
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
s : Set X
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (𝓝 ∘ f) s x

Tactic:
h.nhds

Premises used: ContinuousWithinAt, Filter.Tendsto.nhds
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
h : ContinuousAt f x
⊢ ContinuousAt (𝓝 ∘ f) x

Tactic:
h.nhds

Premises used: ContinuousAt, Filter.Tendsto.nhds
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
h : ContinuousOn f s
⊢ ContinuousOn (𝓝 ∘ f) s

Tactic:
fun x hx => (h x hx).nhds

Premises used: ContinuousWithinAt.nhds, ContinuousOn
-- Module: Mathlib.Topology.Filter
Goal:
X : Type u_4
Y : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : Continuous[inst, inst_1] f
⊢ Continuous[inst, _] (𝓝 ∘ f)

Tactic:
Filter.continuous_nhds.comp h

Premises used: Continuous.comp, Filter.continuous_nhds
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h : IsOpen[inst] s
⊢ ∀ (t : Set X), Membership.mem (γ := Set (Set X)) {s} t → IsOpen[inst] t

Tactic:
simp [h]
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsGδ.{u_1} (X := X) ∅

Tactic:
isOpen_empty.isGδ

Premises used: IsOpen.isGδ, isOpen_empty
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsGδ.{u_1} (X := X) univ

Tactic:
isOpen_univ.isGδ

Premises used: isOpen_univ, IsOpen.isGδ
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf rwa rwa₁ rwa₂ rwa₃ : ∀ ⦃x : ι⦄, x ∈ I → IsOpen[inst] (f x)
⊢ ∀ t ∈ f '' I, IsOpen[inst] t

Tactic:
rwa [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen[inst] (f i)
rw rw₁ : Eq.{u_1 + 1} (α := Set X) (⋂ i ∈ I, f i) (⋂ a ∈ I, f a)
⊢ ⋂ i ∈ I, f i = ⋂₀ (f '' I)

Tactic:
rw [sInter_image]

Premises used: Set.sInter_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hf rwa rwa₁ rwa₂ rwa₃ : ∀ (i : ι'), IsOpen[inst] (f i)
⊢ ∀ t ∈ range f, IsOpen[inst] t

Tactic:
rwa [forall_mem_range]

Premises used: Set.forall_mem_range
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst] (f i)
rw rw₁ : Eq.{u_1 + 1} (α := Set X) (⋂ (i : ι'), f i) (⋂ (x : ι'), f x)
⊢ ⋂ (i : ι'), f i = ⋂₀ range f

Tactic:
rw [sInter_range]

Premises used: Set.sInter_range
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 : IsGδ s → ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n
refine_2 : (∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n) → IsGδ s
⊢ IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ s = ⋂ (n : ℕ), f n

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
refine_1 :
  ∀ (hT : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t)
    (T_count : Set.Countable.{u_1} (α := Set X) ∅),
    ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋂₀ ∅) (⋂ (n : ℕ), f n)
refine_1₁ : ∀ (hT : T.Nonempty), ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n

Tactic:
rcases Set.eq_empty_or_nonempty T with rfl | hT

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
hT : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
⊢ Eq.{u_1 + 1} (α := Set X) (⋂₀ ∅) (⋂ (n : ℕ), (fun (_n : ℕ) ↦ (univ : Set X)) n)

Tactic:
simp
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
hT : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ Eq.{u_1 + 1} (α := Set X) (⋂₀ ∅) (⋂ (n : ℕ), f n)

Tactic:
exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT_1 : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
hT : T.Nonempty
⊢ ∃ (f : ℕ → Set X), T = range f

Tactic:
Countable.exists_eq_range T_count hT

Premises used: Set.Countable.exists_eq_range
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT_1 : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
hT : T.Nonempty
refine_1 :
  ∀ (f : ℕ → Set X) (hf : T = range f), ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n

Tactic:
obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT

Premises used: Set.Countable.exists_eq_range
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT_1 : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∀ (n : ℕ), IsOpen[inst] (f n)

Tactic:
simp_all
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT_1 : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ⋂₀ T = ⋂ (n : ℕ), f n

Tactic:
simp [hf]
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
hT_1 : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
hT : T.Nonempty
f : ℕ → Set X
hf : T = range f
⊢ ∃ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (f n)) ∧ ⋂₀ T = ⋂ (n : ℕ), f n

Tactic:
exact ⟨f, by simp_all, by simp [hf]⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
f : ℕ → Set X
hf : ∀ (n : ℕ), IsOpen[inst] (f n)
⊢ IsGδ.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
.iInter_of_isOpen hf

Premises used: IsGδ.iInter_of_isOpen
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
f : ℕ → Set X
hf : ∀ (n : ℕ), IsOpen[inst] (f n)
⊢ IsGδ.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
exact .iInter_of_isOpen hf
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
s : ι' → Set X
hs : ∀ (i : ι'), IsGδ (s i)
choose :
  ∀ (T : (i : ι') → Set (Set X)) (hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t) (hTc : ∀ (i : ι'), (T i).Countable)
    (hTs : ∀ (i : ι'), s i = ⋂₀ T i), IsGδ.{u_1} (X := X) (⋂ (i : ι'), s i)
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), s i)

Tactic:
choose T hTo hTc hTs using hs
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
s : ι' → Set X
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), s i = ⋂₀ T i
⊢ s = fun (i : ι') ↦ ⋂₀ T i

Tactic:
funext hTs

Premises used: funext
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
s : ι' → Set X
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), s i = ⋂₀ T i
obtain :
  ∀ (hTs : ∀ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i = ⋂₀ T i), IsGδ.{u_1} (X := X) (⋂ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i)
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), s i)

Tactic:
obtain rfl : s = fun i => ⋂₀ T i := funext hTs

Premises used: funext, Set.sInter, rfl
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i)

Tactic:
⟨⋃ i, T i, ?_, countable_iUnion hTc, (sInter_iUnion _).symm⟩

Premises used: Set.sInter_iUnion, Set.countable_iUnion, And.intro, Exists.intro, Eq.symm, IsGδ, Set.iUnion
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i = ⋂₀ T i
refine : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) (⋃ (i : ι'), T i) t → IsOpen[inst] t
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i)

Tactic:
refine ⟨⋃ i, T i, ?_, countable_iUnion hTc, (sInter_iUnion _).symm⟩
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Countable ι'
T : (i : ι') → Set (Set X)
hTo : ∀ (i : ι'), ∀ t ∈ T i, IsOpen[inst] t
hTc : ∀ (i : ι'), (T i).Countable
hTs : ∀ (i : ι'), (fun (i : ι') ↦ ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ (t : Set X), Membership.mem (γ := Set (Set X)) (⋃ (i : ι'), T i) t → IsOpen[inst] t

Tactic:
simpa [@forall_comm ι'] using hTo

Premises used: forall_comm
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
rw : IsGδ.{u_1} (X := X) (⋂ (x : (↑s : Type u_3)), t (↑x : ι) ⋯)
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ι), ⋂ (h : i ∈ s), t i h)

Tactic:
rw [biInter_eq_iInter]

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ Countable.{u_3 + 1} (↑s : Type u_3)

Tactic:
haveI := hs.to_subtype
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Countable.{u_3 + 1} (↑s : Type u_3)
⊢ IsGδ.{u_1} (X := X) (⋂ (x : (↑s : Type u_3)), t (↑x : ι) ⋯)

Tactic:
.iInter fun x => ht x x.2

Premises used: IsGδ.iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Countable
t : (i : ι) → i ∈ s → Set X
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Countable.{u_3 + 1} (↑s : Type u_3)
⊢ IsGδ.{u_1} (X := X) (⋂ (x : (↑s : Type u_3)), t (↑x : ι) ⋯)

Tactic:
exact .iInter fun x => ht x x.2
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
h : ∀ s ∈ S, IsGδ s
hS : S.Countable
⊢ IsGδ (⋂₀ S)

Tactic:
simpa only [sInter_eq_biInter] using IsGδ.biInter hS h

Premises used: Set.sInter_eq_biInter, IsGδ.biInter
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
rw : IsGδ.{u_1} (X := X) (⋂ (b : Bool), bif b then s else t)
⊢ IsGδ (s ∩ t)

Tactic:
rw [inter_eq_iInter]

Premises used: Set.inter_eq_iInter
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ.{u_1} (X := X) (⋂ (b : Bool), bif b then s else t)

Tactic:
.iInter (Bool.forall_bool.2 ⟨ht, hs⟩)

Premises used: Iff.mpr, Bool.forall_bool, IsGδ.iInter, And.intro
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ.{u_1} (X := X) (⋂ (b : Bool), bif b then s else t)

Tactic:
exact .iInter (Bool.forall_bool.2 ⟨ht, hs⟩)
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
rcases : ∀ (S : Set (Set X)) (Sopen : ∀ t ∈ S, IsOpen[inst] t) (Scount : S.Countable), IsGδ (⋂₀ S ∪ t)
⊢ IsGδ (s ∪ t)

Tactic:
rcases hs with ⟨S, Sopen, Scount, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set X
ht : IsGδ t
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
rcases : ∀ (T : Set (Set X)) (Topen : ∀ t ∈ T, IsOpen[inst] t) (Tcount : T.Countable), IsGδ (⋂₀ S ∪ ⋂₀ T)
⊢ IsGδ (⋂₀ S ∪ t)

Tactic:
rcases ht with ⟨T, Topen, Tcount, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
rw : IsGδ.{u_1} (X := X) (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)
⊢ IsGδ (⋂₀ S ∪ ⋂₀ T)

Tactic:
rw [sInter_union_sInter]

Premises used: Set.sInter_union_sInter
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
⊢ IsGδ.{u_1} (X := X) (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)

Tactic:
.biInter_of_isOpen (Scount.prod Tcount) ?_

Premises used: IsGδ.biInter_of_isOpen, Set.Countable.prod
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
refine : ∀ i ∈ S ×ˢ T, IsOpen[inst] (i.1 ∪ i.2)
⊢ IsGδ.{u_1} (X := X) (⋂ p ∈ S ×ˢ T, p.1 ∪ p.2)

Tactic:
refine .biInter_of_isOpen (Scount.prod Tcount) ?_
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
a b : Set X
ha : (a, b).1 ∈ S
hb : (a, b).2 ∈ T
⊢ IsOpen[inst] ((a, b).1 ∪ (a, b).2)

Tactic:
(Sopen a ha).union (Topen b hb)

Premises used: IsOpen.union
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst] t
Scount : S.Countable
T : Set (Set X)
Topen : ∀ t ∈ T, IsOpen[inst] t
Tcount : T.Countable
a b : Set X
ha : (a, b).1 ∈ S
hb : (a, b).2 ∈ T
⊢ IsOpen[inst] ((a, b).1 ∪ (a, b).2)

Tactic:
exact (Sopen a ha).union (Topen b hb)

Premises used: IsOpen.union
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
h : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsGδ s
⊢ IsGδ.{u_1} (X := X) (⋃₀ ∅)

Tactic:
simp
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
a : Set X
s : Set (Set X)
h_1 : a ∉ s
hs : s.Finite
ih : ∀ (h : ∀ s_1 ∈ s, IsGδ s_1), IsGδ (⋃₀ s)
h : ∀ s_1 ∈ Insert.insert a s, IsGδ s_1
insert : ∀ (h : IsGδ a ∧ ∀ x ∈ s, IsGδ x), IsGδ (a ∪ ⋃₀ s)
⊢ IsGδ (⋃₀ Insert.insert a s)

Tactic:
simp only [forall_mem_insert, sUnion_insert] at *

Premises used: Set.forall_mem_insert, Set.sUnion_insert
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
a : Set X
s : Set (Set X)
h_1 : a ∉ s
hs : s.Finite
ih : ∀ (h : ∀ s_1 ∈ s, IsGδ s_1), IsGδ (⋃₀ s)
h : IsGδ a ∧ ∀ x ∈ s, IsGδ x
⊢ IsGδ (a ∪ ⋃₀ s)

Tactic:
h.1.union (ih h.2)

Premises used: IsGδ.union, And.right, And.left
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
a : Set X
s : Set (Set X)
h_1 : a ∉ s
hs : s.Finite
ih : ∀ (h : ∀ s_1 ∈ s, IsGδ s_1), IsGδ (⋃₀ s)
h : IsGδ a ∧ ∀ x ∈ s, IsGδ x
⊢ IsGδ (a ∪ ⋃₀ s)

Tactic:
exact h.1.union (ih h.2)

Premises used: IsGδ.union, And.right, And.left
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
h : ∀ s ∈ S, IsGδ s
empty : ∀ (h : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsGδ s), IsGδ.{u_1} (X := X) (⋃₀ ∅)
insert :
  ∀ {a : Set X} {s : Set (Set X)},
    a ∉ s →
      s.Finite →
        ∀ (ih : ∀ (h : ∀ s_1 ∈ s, IsGδ s_1), IsGδ (⋃₀ s)) (h : ∀ s_1 ∈ Insert.insert a s, IsGδ s_1),
          IsGδ (⋃₀ Insert.insert a s)
⊢ IsGδ (⋃₀ S)

Tactic:
induction S, hS using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp only [forall_mem_insert, sUnion_insert] at *
    exact h.1.union (ih h.2)

Premises used: Set.forall_mem_insert, Set.sUnion_insert, Insert.insert
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
rw : IsGδ (⋃₀ (f '' s))
⊢ IsGδ.{u_1} (X := X) (⋃ i ∈ s, f i)

Tactic:
rw [← sUnion_image]

Premises used: Set.sUnion_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃₀ (f '' s))

Tactic:
.sUnion (hs.image _) (forall_mem_image.2 h)

Premises used: Iff.mpr, Set.Finite.image, IsGδ.sUnion, Set.forall_mem_image
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι : Type u_3
inst : TopologicalSpace X
s : Set ι
hs : s.Finite
f : ι → Set X
h : ∀ i ∈ s, IsGδ (f i)
⊢ IsGδ (⋃₀ (f '' s))

Tactic:
exact .sUnion (hs.image _) (forall_mem_image.2 h)
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
ι' : Sort u_4
inst : TopologicalSpace X
inst_1 : Finite ι'
f : ι' → Set X
h : ∀ (i : ι'), IsGδ (f i)
⊢ IsGδ.{u_1} (X := X) (⋃ (i : ι'), f i)

Tactic:
.sUnion (finite_range _) <| forall_mem_range.2 h

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Set.finite_range, Set.iUnion, IsGδ.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
s : Set Y
hf : Continuous[inst, inst_1] f
hs : IsGδ s
obtain : ∀ (U : ℕ → Set Y) (hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)) (hU2 : s = ⋂ (n : ℕ), U n), IsGδ (f ⁻¹' s)
⊢ IsGδ (f ⁻¹' s)

Tactic:
obtain ⟨U, hU1, hU2⟩ := hs.eq_iInter_nat

Premises used: IsGδ.eq_iInter_nat
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst, inst_1] f
hs : IsGδ s
U : ℕ → Set Y
hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU2 : s = ⋂ (n : ℕ), U n
simp_all :
  ∀ (hs : IsGδ.{u_2} (X := Y) (⋂ (n : ℕ), U n)) (hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)) (hU2 : s = ⋂ (n : ℕ), U n),
    IsGδ.{u_1} (X := X) (⋂ (i : ℕ), f ⁻¹' U i)
⊢ IsGδ (f ⁻¹' s)

Tactic:
simp_all only [preimage_iInter]

Premises used: Set.preimage_iInter
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst, inst_1] f
U : ℕ → Set Y
hs : IsGδ.{u_2} (X := Y) (⋂ (n : ℕ), U n)
hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU2 : s = ⋂ (n : ℕ), U n
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ℕ), f ⁻¹' U i)

Tactic:
IsGδ.iInter_of_isOpen (fun i => hf.isOpen_preimage (U i) (hU1 i))

Premises used: Continuous.isOpen_preimage, IsGδ.iInter_of_isOpen
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hf : Continuous[inst, inst_1] f
U : ℕ → Set Y
hs : IsGδ.{u_2} (X := Y) (⋂ (n : ℕ), U n)
hU1 : ∀ (n : ℕ), IsOpen[inst_1] (U n)
hU2 : s = ⋂ (n : ℕ), U n
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ℕ), f ⁻¹' U i)

Tactic:
exact IsGδ.iInter_of_isOpen (fun i => hf.isOpen_preimage (U i) (hU1 i))

Premises used: Continuous.isOpen_preimage, IsGδ.iInter_of_isOpen
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_3
ι' : Sort u_4
inst : TopologicalSpace X
⊢ CountableInterFilter.{u_1} (α := X) (countableGenerate {t : Set X | IsOpen[inst] t ∧ Dense t})

Tactic:
infer_instance
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
ho : IsOpen[inst] s
hd : Dense s
⊢ s ∈ residual X

Tactic:
CountableGenerateSets.basic ⟨ho, hd⟩

Premises used: Set.Mem, And.intro, Filter.CountableGenerateSets.basic
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
ho : IsGδ s
hd : Dense s
rcases : ∀ (T : Set (Set X)) (To : ∀ t ∈ T, IsOpen[inst] t) (Tct : T.Countable) (hd : Dense (⋂₀ T)), ⋂₀ T ∈ residual X
⊢ s ∈ residual X

Tactic:
rcases ho with ⟨T, To, Tct, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
To : ∀ t ∈ T, IsOpen[inst] t
Tct : T.Countable
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual X

Tactic:
(countable_sInter_mem Tct).mpr fun t tT =>
      residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))

Premises used: Iff.mpr, Dense.mono, Set.sInter_subset_of_mem, residual_of_dense_open, countable_sInter_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Set (Set X)
To : ∀ t ∈ T, IsOpen[inst] t
Tct : T.Countable
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual X

Tactic:
exact
    (countable_sInter_mem Tct).mpr fun t tT =>
      residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))

Premises used: Iff.mpr, Dense.mono, Set.sInter_subset_of_mem, residual_of_dense_open, countable_sInter_mem
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp_rw :
  (∃ (S : Set (Set X)),
      (∀ x ∈ S, Membership.mem (γ := Set (Set X)) {t : Set X | IsOpen[inst] t ∧ Dense t} x) ∧
        S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
simp_rw₁ :
  (∃ (S : Set (Set X)), (∀ x ∈ S, IsOpen[inst] x ∧ Dense x) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
simp_rw₂ :
  (∃ (S : Set (Set X)),
      ((∀ (x : Set X) (x_1 : x ∈ S), IsOpen[inst] x) ∧ ∀ (x : Set X) (x_1 : x ∈ S), Dense x) ∧
        S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ∀ x ∈ ⋂₀ S, x ∈ s
⊢ (∃ S ⊆ {t : Set X | IsOpen[inst] t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ (S : Set (Set X)), (∀ t ∈ S, IsOpen[inst] t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
simp_rw [subset_def, mem_setOf, forall_and, and_assoc]

Premises used: Set.subset_def, Set.mem_setOf, and_assoc, forall_and
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (interior (closure[inst] ∅)) ∅
rw₁ : Eq.{u_1 + 1} (α := Set X) (interior ∅) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
⊢ IsNowhereDense.{u_1} (X := X) ∅

Tactic:
rw [IsNowhereDense, closure_empty, interior_empty]

Premises used: interior_empty, closure_empty, IsNowhereDense
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
grw : interior (closure[inst] s) ⊆ ∅
⊢ interior (closure[inst] t) ⊆ ∅

Tactic:
grw [ht]
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
ht : t ⊆ s
hs : IsNowhereDense s
rw rw₁ : Subset.{u_1} (α := Set X) ∅ ∅
⊢ interior (closure[inst] s) ⊆ ∅

Tactic:
rw [hs]
-- Module: Mathlib.Topology.GDelta.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
rw : interior (closure[inst] s) = ∅ ↔ interior s = ∅
rw₁ rw₂ : interior s = ∅ ↔ interior s = ∅
⊢ IsNowhereDense s ↔ interior s = ∅

Tactic:
rw [IsNowhereDense, IsClosed.closure_eq hs]

Premises used: IsClosed.closure_eq, IsNowhereDense