awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ w ⊆ ⋃ a ∈ s u, a

Tactic:
exact subset_iUnion₂_of_subset w ws (Subset.refl _)

Premises used: Set.Subset.refl, Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
⊢ IsTopologicalBasis t'

Tactic:
have : IsTopologicalBasis t' := TopologicalSpace.isTopologicalBasis_of_subbasis ht
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
⊢ ∃ s' ⊆ t', s'.Countable ∧ IsTopologicalBasis s'

Tactic:
this.exists_countable

Premises used: TopologicalSpace.IsTopologicalBasis.exists_countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
obtain :
  ∀ (s' : Set (Set α)) (s't' : s' ⊆ t') (s'_count : s'.Countable) (hs' : IsTopologicalBasis s'),
    ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

Tactic:
obtain ⟨s', s't', s'_count, hs'⟩ : ∃ s' ⊆ t', s'.Countable ∧ IsTopologicalBasis s' :=
    this.exists_countable

Premises used: TopologicalSpace.IsTopologicalBasis.exists_countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
u : Set α
hu : u ∈ s'
⊢ ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u

Tactic:
simpa [t', and_assoc] using s't' hu

Premises used: and_assoc
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
⊢ ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u

Tactic:
have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u :=
    fun u hu ↦ by simpa [t', and_assoc] using s't' hu
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u
choose! :
  ∀ (f : (u : Set α) → Set (Set α)) (f_fin : ∀ u ∈ s', (f u).Finite) (ft : ∀ u ∈ s', f u ⊆ t)
    (hf : ∀ u ∈ s', ⋂₀ f u = u), ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

Tactic:
choose! f f_fin ft hf using A
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ⋃ u ∈ s', f u ⊆ t

Tactic:
simpa using ft
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_1 : Set.Countable.{u_1} (α := Set α) (⋃ u ∈ s', f u)
refine_2 : ts = generateFrom (⋃ u ∈ s', f u)
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

Tactic:
refine ⟨⋃ u ∈ s', f u, by simpa using ft, ?_, ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_1 : ∀ (a : Set α) (ha : a ∈ s'), (f a).Countable
⊢ Set.Countable.{u_1} (α := Set α) (⋃ u ∈ s', f u)

Tactic:
apply s'_count.biUnion

Premises used: Set.Countable.biUnion
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ (f u).Countable

Tactic:
Finite.countable (f_fin u hu)

Premises used: Set.Finite.countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ (f u).Countable

Tactic:
exact Finite.countable (f_fin u hu)

Premises used: Set.Finite.countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_2 : ts ≤ generateFrom (⋃ u ∈ s', f u)
refine_2₁ : generateFrom (⋃ u ∈ s', f u) ≤ ts
⊢ ts = generateFrom (⋃ u ∈ s', f u)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_2 : Subset.{u_1} (α := Set (Set α)) (⋃ u ∈ s', f u) {s : Set α | IsOpen[ts] s}
⊢ ts ≤ generateFrom (⋃ u ∈ s', f u)

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Premises used: Iff.mpr, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_2 : ∀ (i : Set α) (i_1 : i ∈ s'), f i ⊆ {s : Set α | IsOpen[ts] s}
⊢ Subset.{u_1} (α := Set (Set α)) (⋃ u ∈ s', f u) {s : Set α | IsOpen[ts] s}

Tactic:
simp only [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
hv : v ∈ f u
refine_2 : Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom t] s} v
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[ts] s} v

Tactic:
rw [ht]
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
hv : v ∈ f u
refine_2 : v ∈ t
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom t] s} v

Tactic:
apply isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
hv : v ∈ f u
⊢ v ∈ t

Tactic:
ft u hu hv
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
v : Set α
hv : v ∈ f u
⊢ v ∈ t

Tactic:
exact ft u hu hv
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_2 : generateFrom (⋃ u ∈ s', f u) ≤ generateFrom s'
⊢ generateFrom (⋃ u ∈ s', f u) ≤ ts

Tactic:
rw [hs'.eq_generateFrom]

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_2 : s' ⊆ {s : Set α | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
⊢ generateFrom (⋃ u ∈ s', f u) ≤ generateFrom s'

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Premises used: Iff.mpr, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
refine_2 : Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom (⋃ u ∈ s', f u)] s} (⋂ i ∈ f u, i)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[generateFrom (⋃ u ∈ s', f u)] s} u

Tactic:
rw [← hf u hu, sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
refine_2 : (f u).Finite
refine_2₁ : ∀ i ∈ f u, IsOpen[generateFrom (⋃ u ∈ s', f u)] i
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] (⋂ i ∈ f u, i)

Tactic:
apply @Finite.isOpen_biInter _ _ (generateFrom (⋃ u ∈ s', f u)) _ _

Premises used: Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ (f u).Finite

Tactic:
apply f_fin u hu
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
hi : i ∈ f u
refine_2 : Membership.mem (γ := Set (Set α)) (⋃ u ∈ s', f u) i
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] i

Tactic:
apply isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
hi : i ∈ f u
refine_2 : ∃ i_1 ∈ s', i ∈ f i_1
⊢ Membership.mem (γ := Set (Set α)) (⋃ u ∈ s', f u) i

Tactic:
simp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
hi : i ∈ f u
⊢ ∃ i_1 ∈ s', i ∈ f i_1

Tactic:
grind
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ IsTopologicalBasis (α := (i : ι) × E i)
    (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i)

Tactic:
.of_hasBasis_nhds fun a ↦ ?_

Premises used: TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
refine :
  ∀ (a : (i : ι) × E i),
    (𝓝 a).HasBasis
      (fun (t : Set ((i : ι) × E i)) ↦
        Membership.mem (γ := Set (Set ((i : ι) × E i)))
            (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
          a ∈ t)
      id
⊢ IsTopologicalBasis (α := (i : ι) × E i)
    (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i)

Tactic:
refine .of_hasBasis_nhds fun a ↦ ?_
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
rw :
  (map (Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)))
        (𝓝 (a.snd (β := fun (i : ι) ↦ E i)))).HasBasis
    (fun (t : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
        a ∈ t)
    id
⊢ (𝓝 a).HasBasis
    (fun (t : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
        a ∈ t)
    id

Tactic:
rw [Sigma.nhds_eq]

Premises used: Sigma.nhds_eq
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
⊢ (map (Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)))
        (𝓝 (a.snd (β := fun (i : ι) ↦ E i)))).HasBasis
    (fun (x : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
        ((fun (i : Set (E (a.fst (β := fun (i : ι) ↦ E i)))) ↦
            Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)) '' i) ''
          {i : Set (E (a.fst (β := fun (i : ι) ↦ E i))) |
            Membership.mem (γ := Set (Set (E (a.fst (β := fun (i : ι) ↦ E i))))) (s (a.fst (β := fun (i : ι) ↦ E i)))
                i ∧
              a.snd (β := fun (i : ι) ↦ E i) ∈ i})
        x)
    id

Tactic:
(((hs a.1).nhds_hasBasis).map _).to_image_id

Premises used: Sigma.fst, Filter.HasBasis.map, Filter.HasBasis.to_image_id, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
h :
  ∀ (x : Set ((i : ι) × E i)),
    Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) x ∧
        a ∈ x ↔
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
        ((fun (i : Set (E (a.fst (β := fun (i : ι) ↦ E i)))) ↦
            Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)) '' i) ''
          {i : Set (E (a.fst (β := fun (i : ι) ↦ E i))) |
            Membership.mem (γ := Set (Set (E (a.fst (β := fun (i : ι) ↦ E i))))) (s (a.fst (β := fun (i : ι) ↦ E i)))
                i ∧
              a.snd (β := fun (i : ι) ↦ E i) ∈ i})
        x
⊢ (map (Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)))
        (𝓝 (a.snd (β := fun (i : ι) ↦ E i)))).HasBasis
    (fun (t : Set ((i : ι) × E i)) ↦
      Membership.mem (γ := Set (Set ((i : ι) × E i)))
          (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) t ∧
        a ∈ t)
    id

Tactic:
convert! (((hs a.1).nhds_hasBasis).map _).to_image_id

Premises used: Sigma.fst, Filter.HasBasis.map, Filter.HasBasis.to_image_id, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
a : (i : ι) × E i
x : Set ((i : ι) × E i)
⊢ Membership.mem (γ := Set (Set ((i : ι) × E i)))
        (⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' s i) x ∧
      a ∈ x ↔
    Membership.mem (γ := Set (Set ((i : ι) × E i)))
      ((fun (i : Set (E (a.fst (β := fun (i : ι) ↦ E i)))) ↦
          Sigma.mk (β := fun (i : ι) ↦ E i) (a.fst (β := fun (i : ι) ↦ E i)) '' i) ''
        {i : Set (E (a.fst (β := fun (i : ι) ↦ E i))) |
          Membership.mem (γ := Set (Set (E (a.fst (β := fun (i : ι) ↦ E i))))) (s (a.fst (β := fun (i : ι) ↦ E i))) i ∧
            a.snd (β := fun (i : ι) ↦ E i) ∈ i})
      x

Tactic:
aesop
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (E i)
b : Set (Set ((i : ι) × E i)) :=
  ⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' countableBasis (E i)
⊢ IsTopologicalBasis b

Tactic:
have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (E i)
b : Set (Set ((i : ι) × E i)) :=
  ⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
⊢ b.Countable

Tactic:
have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (E i)
b : Set (Set ((i : ι) × E i)) :=
  ⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology ((i : ι) × E i)

Tactic:
A.secondCountableTopology B

Premises used: TopologicalSpace.IsTopologicalBasis.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → TopologicalSpace (E i)
inst_1 : Countable ι
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_2} (E i)
b : Set (Set ((i : ι) × E i)) :=
  ⋃ (i : ι), (fun (u : Set (E i)) ↦ Sigma.mk (β := fun (i : ι) ↦ E i) i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology ((i : ι) × E i)

Tactic:
exact A.secondCountableTopology B

Premises used: TopologicalSpace.IsTopologicalBasis.secondCountableTopology