awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
hi : i ∈ s
⊢ IsOpen[inst i] (U i)

Tactic:
exact hU _ hi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
hi : i ∉ s
neg : IsOpen[inst i] univ
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)

Tactic:
rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]

Premises used: if_pos, Set.eval_image_pi_of_notMem
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst i] univ

Tactic:
isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : ((↑s : Set ι).pi (α := X) U).Nonempty
hi : i ∉ s
⊢ IsOpen[inst i] univ

Tactic:
exact isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
refine₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inl :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inr inr₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : ((↑s : Set ι).pi (α := X) U).Nonempty), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
pos :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : ((↑s : Set ι).pi (α := X) U).Nonempty) (hi : i ∈ s),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
neg neg₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : ((↑s : Set ι).pi (α := X) U).Nonempty) (hi : i ∉ s),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)

Tactic:
classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ

Premises used: Iff.mpr, TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, TopologicalSpace.isTopologicalBasis_opens, isOpen_univ, isTopologicalBasis_pi, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t

Tactic:
let ⟨t, htc, htd⟩ := exists_countable_dense s
  ⟨(↑) '' t, Subtype.coe_image_subset s t, htc.image Subtype.val,
    hs.denseRange_val.dense_image continuous_subtype_val htd⟩

Premises used: _private.0.Dense.exists_countable_dense_subset.match_1, Exists, Dense, Set.Elem, HasSubset.Subset, TopologicalSpace.exists_countable_dense, And, And.intro, Exists.intro, Set.image, Set.Countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
rcases :
  ∀ (t : Set α) (hts : t ⊆ s) (htc : t.Countable) (htd : Dense t),
    ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩

Premises used: Dense.exists_countable_dense_subset
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩

Premises used: setOf, IsBot, Inter.inter, And.intro, Exists.intro, IsTop, Union.union
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s
refine_2 : ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s).Countable
refine_3 : Dense ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s)
refine_4 : ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s
refine_5 : ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s).Countable

Tactic:
(htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left

Premises used: Set.inter_subset_left, Set.Countable.union, Set.countable_isTop, Set.Countable.mono, Set.countable_isBot
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s)

Tactic:
htd.mono (subset_inter subset_union_left hts)

Premises used: Dense.mono, Set.subset_union_left, Set.subset_inter
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s

Tactic:
fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, Or.inl, Or.inr
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s

Tactic:
fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, Or.inr
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s

Tactic:
exacts [inter_subset_right,
    (htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left,
    htd.mono (subset_inter subset_union_left hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩,
    fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩]

Premises used: Dense.mono, Set.inter_subset_left, Set.Countable.union, Set.subset_union_left, Set.subset_inter, Set.countable_isTop, Set.Countable.mono, Set.countable_isBot, Set.inter_subset_right
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SeparableSpace α
⊢ SeparableSpace.{u_1} (↑univ : Type u_1)

Tactic:
(Equiv.Set.univ α).symm.surjective.denseRange.separableSpace (continuous_id.subtype_mk _)

Premises used: Function.Surjective.denseRange, Continuous.subtype_mk, DenseRange.separableSpace, continuous_id, Equiv.surjective, Equiv.symm, Equiv.Set.univ
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : SeparableSpace α
inst_2 : PartialOrder α
⊢ ∃ (s : Set α), s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s

Tactic:
simpa using dense_univ.exists_countable_dense_subset_bot_top

Premises used: Dense.exists_countable_dense_subset_bot_top, dense_univ
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : FirstCountableTopology β
f : α → β
⊢ FirstCountableTopology α

Tactic:
let _ := t.induced f
  ⟨fun x ↦ nhds_induced f x ▸ inferInstance⟩

Premises used: Eq.rec, inferInstance, TopologicalSpace.induced, nhds_induced, FirstCountableTopology.mk, Eq.symm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
inst : FirstCountableTopology α
⊢ FirstCountableTopology.{u} (↑s : Type u)

Tactic:
firstCountableTopology_induced s α (↑)

Premises used: Set.Elem, Subtype.val, TopologicalSpace.firstCountableTopology_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology β
f : α → β
hf : IsInducing f
rw : FirstCountableTopology α
⊢ FirstCountableTopology α

Tactic:
rw [hf.1]

Premises used: Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
firstCountableTopology_induced α β f

Premises used: TopologicalSpace.firstCountableTopology_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α

Tactic:
exact firstCountableTopology_induced α β f

Premises used: TopologicalSpace.firstCountableTopology_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology β
f : α → β
hf : IsEmbedding f
⊢ FirstCountableTopology α

Tactic:
hf.1.firstCountableTopology

Premises used: Topology.IsEmbedding.toIsInducing, Topology.IsInducing.firstCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
x : α
f : Filter α
inst_1 : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
obtain : ∀ (g : ℕ → α) (hg : Tendsto g atTop (𝓝 x ⊓ f)), ∃ (ψ : ℕ → α), Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f
⊢ ∃ (ψ : ℕ → α), Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
obtain ⟨g, hg⟩ := Filter.exists_seq_tendsto (𝓝 x ⊓ f)

Premises used: nhds, Filter.exists_seq_tendsto, Min.min
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
x : α
f : Filter α
inst_1 : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
g : ℕ → α
hg : Tendsto g atTop (𝓝 x ⊓ f)
⊢ ∃ (ψ : ℕ → α), Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
⟨g, (tendsto_inf.1 hg).1, (tendsto_inf.1 hg).2⟩

Premises used: Filter.tendsto_inf, And.right, And.left, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
x : α
f : Filter α
inst_1 : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
g : ℕ → α
hg : Tendsto g atTop (𝓝 x ⊓ f)
⊢ ∃ (ψ : ℕ → α), Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
exact ⟨g, (tendsto_inf.1 hg).1, (tendsto_inf.1 hg).2⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
ι : Type u_1
f : Filter ι
inst_1 : f.IsCountablyGenerated
x : α
u : ι → α
hx : MapClusterPt x f u
⊢ ∃ (ψ : ℕ → ι), Tendsto (u ∘ ψ) atTop (𝓝 x) ∧ Tendsto ψ atTop f

Tactic:
grind [exists_seq_comp_tendsto hx]

Premises used: Filter.exists_seq_comp_tendsto
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
x : α
u : ℕ → α
hx : MapClusterPt x atTop u
⊢ ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x)

Tactic:
subseq_tendsto_of_neBot hx

Premises used: Filter.subseq_tendsto_of_neBot
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
u : ℕ → α
x : α
hx : MapClusterPt x atTop u
⊢ ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x)

Tactic:
subseq_tendsto_of_neBot hx

Premises used: Filter.subseq_tendsto_of_neBot
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology α
inst_2 : FirstCountableTopology β
x_1 : α × β
x : α
y : β
rw : (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated
⊢ (𝓝 (x, y)).IsCountablyGenerated

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology α
inst_2 : FirstCountableTopology β
x_1 : α × β
x : α
y : β
⊢ (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated

Tactic:
infer_instance
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst : Countable ι
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), FirstCountableTopology.{u_2} (X i)
f : (i : ι) → X i
rw : IsCountablyGenerated (α := (i : ι) → X i) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (f i))
⊢ (𝓝 f).IsCountablyGenerated

Tactic:
rw [nhds_pi]

Premises used: nhds_pi
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst : Countable ι
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), FirstCountableTopology.{u_2} (X i)
f : (i : ι) → X i
⊢ IsCountablyGenerated (α := (i : ι) → X i) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (f i))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
x : α
inst : (𝓝 x).IsCountablyGenerated
s : Set α
⊢ (𝓝[s] x).IsCountablyGenerated

Tactic:
Inf.isCountablyGenerated _ _

Premises used: Filter.Inf.isCountablyGenerated, nhdsWithin
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
hc : b.Countable
⊢ SecondCountableTopology α

Tactic:
⟨⟨b, hc, hb.eq_generateFrom⟩⟩

Premises used: SecondCountableTopology.mk, TopologicalSpace.IsTopologicalBasis.eq_generateFrom, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
b : Set (Set α)
hc : b.Countable
⊢ SecondCountableTopology α

Tactic:
@SecondCountableTopology.mk α (generateFrom b) ⟨b, hc, rfl⟩

Premises used: SecondCountableTopology.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
obtain :
  ∀ (b : Set (Set α)) (hb₁ : b.Countable) (hb₂ : t = generateFrom b),
    ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b
⊢ ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _

Premises used: SecondCountableTopology.is_open_generated_countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
⟨_, ?_, notMem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩

Premises used: TopologicalSpace.IsTopologicalBasis.diff_empty, Set.notMem_diff_of_mem, TopologicalSpace.isTopologicalBasis_of_subbasis, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
refine_1 : Set.Countable (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ b} \ {∅})
refine_2 : Membership.mem (γ := Set (Set α)) {∅} ∅
⊢ ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Tactic:
refine ⟨_, ?_, notMem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ Set.Countable (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ b} \ {∅})

Tactic:
((countable_setOf_finite_subset hb₁).image _).mono diff_subset

Premises used: Set.diff_subset, Set.Countable.image, Set.Countable.mono, Set.countable_setOf_finite_subset
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ Membership.mem (γ := Set (Set α)) {∅} ∅

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.singleton, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ Set.Countable (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ b} \ {∅})

Tactic:
exacts [((countable_setOf_finite_subset hb₁).image _).mono diff_subset, rfl]

Premises used: Set.diff_subset, Set.Countable.image, Set.Countable.mono, rfl, Set.countable_setOf_finite_subset
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
obtain :
  ∀ (t_1 : Set (Set α)) (ht : t_1.Countable ∧ ∅ ∉ t_1 ∧ IsTopologicalBasis t_1),
    ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)

Tactic:
obtain ⟨t, ht⟩ := TopologicalSpace.exists_countable_basis α

Premises used: TopologicalSpace.exists_countable_basis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
pos : ∀ (hn : t.Nonempty), ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
neg : ∀ (hn : t = ∅), ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)

Tactic:
by_cases! hn : t.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t.Nonempty
pos :
  ∀ (b : ℕ → Set α) (ht : (range b).Countable ∧ ∅ ∉ range b ∧ IsTopologicalBasis (range b)) (hn : (range b).Nonempty),
    ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)

Tactic:
obtain ⟨b, rfl⟩ := ht.1.exists_eq_range hn

Premises used: And.left, Set.Countable.exists_eq_range, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : ℕ → Set α
ht : (range b).Countable ∧ ∅ ∉ range b ∧ IsTopologicalBasis (range b)
hn : (range b).Nonempty
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)

Tactic:
⟨b, ht.2.2⟩

Premises used: And.right, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : ℕ → Set α
ht : (range b).Countable ∧ ∅ ∉ range b ∧ IsTopologicalBasis (range b)
hn : (range b).Nonempty
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)

Tactic:
exact ⟨b, ht.2.2⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t = ∅
⊢ IsTopologicalBasis.{u} (α := α) (range fun (n : ℕ) ↦ ∅)

Tactic:
simp_all
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t = ∅
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)

Tactic:
exact ⟨fun n => ∅, by simp_all⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ (countableBasis α).Countable

Tactic:
(exists_countable_basis α).choose_spec.1

Premises used: Exists.choose_spec, TopologicalSpace.countableBasis, TopologicalSpace.exists_countable_basis, And.left
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ ∅ ∉ countableBasis α

Tactic:
(exists_countable_basis α).choose_spec.2.1

Premises used: Exists.choose_spec, TopologicalSpace.countableBasis, Set.Mem, TopologicalSpace.exists_countable_basis, And.right, And.left
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ IsTopologicalBasis (countableBasis α)

Tactic:
(exists_countable_basis α).choose_spec.2.2

Premises used: Exists.choose_spec, TopologicalSpace.countableBasis, TopologicalSpace.exists_countable_basis, And.right
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ t = generateFrom (countableBasis α)

Tactic:
(isBasis_countableBasis α).eq_generateFrom

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom, TopologicalSpace.isBasis_countableBasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
s : Set α
hs : s ∈ countableBasis α
⊢ IsOpen[t] s

Tactic:
(isBasis_countableBasis α).isOpen hs

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.isBasis_countableBasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
s : Set α
hs : s ∈ countableBasis α
⊢ s.Nonempty

Tactic:
nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs <| empty_notMem_countableBasis α

Premises used: Iff.mpr, TopologicalSpace.empty_notMem_countableBasis, ne_of_mem_of_not_mem, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ FirstCountableTopology α

Tactic:
⟨fun _ => HasCountableBasis.isCountablyGenerated <|
      ⟨(isBasis_countableBasis α).nhds_hasBasis,
        (countable_countableBasis α).mono inter_subset_left⟩⟩

Premises used: Filter.HasCountableBasis.mk, TopologicalSpace.countable_countableBasis, Set.inter_subset_left, Filter.HasCountableBasis.isCountablyGenerated, Set.Countable.mono, TopologicalSpace.isBasis_countableBasis, FirstCountableTopology.mk, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis