awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
choose :
  ∀ (b : (x : α) → ℕ → Set α) (hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i))
    (hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i), ∃ (b : Set (Set α)), b.Countable ∧ t = generateFrom b
⊢ ∃ (b : Set (Set α)), b.Countable ∧ t = generateFrom b

Tactic:
choose b hxb hbb using fun x : α => (nhds_basis_opens x).exists_antitone_subbasis

Premises used: Filter.HasBasis.exists_antitone_subbasis, nhds_basis_opens
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
right : t = generateFrom (range (uncurry b))
⊢ ∃ (b : Set (Set α)), b.Countable ∧ t = generateFrom b

Tactic:
use range b.uncurry, countable_range b.uncurry

Premises used: Set.countable_range, Set.range, Function.uncurry
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
right : t ≤ generateFrom (range (uncurry b))
right₁ : generateFrom (range (uncurry b)) ≤ t
⊢ t = generateFrom (range (uncurry b))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
right : range (uncurry b) ⊆ {s : Set α | IsOpen[t] s}
⊢ t ≤ generateFrom (range (uncurry b))

Tactic:
rw [le_generateFrom_iff_subset_isOpen]

Premises used: TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[t] s} (uncurry b (x, n))

Tactic:
(hxb x n).right

Premises used: Set.Mem, setOf, And.right, IsOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[t] s} (uncurry b (x, n))

Tactic:
exact (hxb x n).right

Premises used: And.right
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
right : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ generateFrom (range (uncurry b)) ≤ t

Tactic:
rw [le_iff_nhds]

Premises used: le_iff_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
right : ∀ (i' : ℕ), True → b x i' ∈ 𝓝 x
⊢ 𝓝 x ≤ 𝓝 x

Tactic:
rw [(hbb x).ge_iff]

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.ge_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
right : True → b x n ∈ 𝓝 x
⊢ True → b x n ∈ 𝓝 x

Tactic:
_
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
h : True
⊢ b x n ∈ 𝓝 x

Tactic:
@IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left

Premises used: And.left, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
h : True
right : IsOpen[generateFrom (range (uncurry b))] (b x n)
⊢ b x n ∈ 𝓝 x

Tactic:
refine @IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left

Premises used: And.left, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
h : True
⊢ IsOpen[generateFrom (range (uncurry b))] (b x n)

Tactic:
isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩

Premises used: Prod.mk, TopologicalSpace.isOpen_generateFrom_of_mem, Exists.intro, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
h : True
⊢ IsOpen[generateFrom (range (uncurry b))] (b x n)

Tactic:
exact isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
rcases : ∀ (b : Set (Set β)) (hb : b.Countable) (eq : t = generateFrom b), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩

Premises used: SecondCountableTopology.is_open_generated_countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α

Tactic:
{ is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }

Premises used: SecondCountableTopology.mk, Set.Countable.image, Set.preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
refine : induced f t = generateFrom (preimage f '' b)
⊢ SecondCountableTopology α

Tactic:
refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
rw : induced f (generateFrom b) = generateFrom (preimage f '' b)
rw₁ rw₂ : generateFrom (preimage f '' b) = generateFrom (preimage f '' b)
⊢ induced f t = generateFrom (preimage f '' b)

Tactic:
rw [eq, induced_generateFrom_eq]

Premises used: induced_generateFrom_eq
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
inst : SecondCountableTopology α
⊢ SecondCountableTopology.{u} (↑s : Type u)

Tactic:
secondCountableTopology_induced s α (↑)

Premises used: Set.Elem, TopologicalSpace.secondCountableTopology_induced, Subtype.val
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ι : Sort u_2
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
rw : SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]

Premises used: generateFrom_iUnion, funext, TopologicalSpace.eq_generateFrom_countableBasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ι : Sort u_2
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
SecondCountableTopology.mk' <|
    countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

Premises used: TopologicalSpace.SecondCountableTopology.mk', TopologicalSpace.countable_countableBasis, Set.countable_iUnion
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
ι : Sort u_2
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
exact SecondCountableTopology.mk' <|
    countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

Premises used: TopologicalSpace.SecondCountableTopology.mk', TopologicalSpace.countable_countableBasis, Set.countable_iUnion
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
⊢ SecondCountableTopology (α × β)

Tactic:
((isBasis_countableBasis α).prod (isBasis_countableBasis β)).secondCountableTopology <|
    (countable_countableBasis α).image2 (countable_countableBasis β) _

Premises used: Set.Countable.image2, TopologicalSpace.countable_countableBasis, TopologicalSpace.IsTopologicalBasis.prod, TopologicalSpace.isBasis_countableBasis, TopologicalSpace.IsTopologicalBasis.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst : Countable ι
inst_1 : (a : ι) → TopologicalSpace (X a)
inst_2 : ∀ (a : ι), SecondCountableTopology.{u_2} (X a)
⊢ SecondCountableTopology ((a : ι) → X a)

Tactic:
secondCountableTopology_iInf fun _ => secondCountableTopology_induced _ _ _

Premises used: TopologicalSpace.secondCountableTopology_iInf, TopologicalSpace.secondCountableTopology_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
choose :
  ∀ (p : (s : (↑(countableBasis α) : Type u)) → α) (hp : ∀ (s : (↑(countableBasis α) : Type u)), p s ∈ (↑s : Set α)),
    SeparableSpace α
⊢ SeparableSpace α

Tactic:
choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2

Premises used: TopologicalSpace.nonempty_of_mem_countableBasis, Subtype.property
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
p : (s : (↑(countableBasis α) : Type u)) → α
hp : ∀ (s : (↑(countableBasis α) : Type u)), p s ∈ (↑s : Set α)
⊢ SeparableSpace α

Tactic:
⟨⟨range p, countable_range _, (isBasis_countableBasis α).dense_iff.2 fun o ho _ =>
          ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩

Premises used: Set.mem_range_self, Iff.mpr, Set.countable_range, Subtype.mk, And.intro, Exists.intro, TopologicalSpace.isBasis_countableBasis, Set.range, TopologicalSpace.SeparableSpace.mk, TopologicalSpace.IsTopologicalBasis.dense_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
p : (s : (↑(countableBasis α) : Type u)) → α
hp : ∀ (s : (↑(countableBasis α) : Type u)), p s ∈ (↑s : Set α)
⊢ SeparableSpace α

Tactic:
exact ⟨⟨range p, countable_range _, (isBasis_countableBasis α).dense_iff.2 fun o ho _ =>
          ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_1
inst : Countable ι
U : ι → Set α
inst_1 : ∀ (i : ι), SecondCountableTopology.{u} (↑(U i) : Type u)
Uo : ∀ (i : ι), IsOpen[t] (U i)
hc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
⊢ SecondCountableTopology α

Tactic:
haveI : IsTopologicalBasis (⋃ i, image ((↑) : U i → α) '' countableBasis (U i)) :=
    isTopologicalBasis_of_cover Uo hc fun i => isBasis_countableBasis (U i)
  this.secondCountableTopology (countable_iUnion fun _ => (countable_countableBasis _).image _)

Premises used: TopologicalSpace.countable_countableBasis, Membership.mem, TopologicalSpace.isTopologicalBasis_of_cover, Set.Elem, Subtype, Set.Countable.image, Set.countable_iUnion, TopologicalSpace.isBasis_countableBasis, Set.image, Subtype.val, TopologicalSpace.IsTopologicalBasis.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
choose :
  ∀ (f : (b : (↑B : Type u)) → ι) (hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)),
    ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)

Tactic:
choose f hf using fun b : B => b.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
⊢ Countable.{u + 1} (↑B : Type u)

Tactic:
haveI : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)

Tactic:
⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩

Premises used: Set.sUnion_subset, Set.countable_range, Set.iUnion₂_subset_iUnion, HasSubset.Subset.antisymm, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
refine : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) (range fun (i : ι) ↦ s i) t' → t' ⊆ ⋃ i ∈ range f, s i
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)

Tactic:
refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
i : ι
x : α
xs : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i) i) x
rcases :
  ∀ (b : Set α) (hb : b ∈ countableBasis α) (xb : x ∈ b) (bs : b ⊆ (fun (i : ι) ↦ s i) i),
    Membership.mem (γ := Set α) (⋃ i ∈ range f, s i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ range f, s i) x

Tactic:
rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩

Premises used: TopologicalSpace.isBasis_countableBasis, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
i : ι
x : α
xs : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i) i) x
b : Set α
hb : b ∈ countableBasis α
xb : x ∈ b
bs : b ⊆ (fun (i : ι) ↦ s i) i
⊢ Membership.mem (γ := Set α) (⋃ i ∈ range f, s i) x

Tactic:
⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩

Premises used: Set.Mem, iSup, setOf, Subtype.mk, And.intro, Exists.intro, Set.iUnion, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
i : ι
x : α
xs : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i) i) x
b : Set α
hb : b ∈ countableBasis α
xb : x ∈ b
bs : b ⊆ (fun (i : ι) ↦ s i) i
⊢ Membership.mem (γ := Set α) (⋃ i ∈ range f, s i) x

Tactic:
exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
simp_rw :
  ∃ (s_1 : Set (↑I : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
      Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)
⊢ ∃ T ⊆ I, T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ i ∈ I, s i)

Tactic:
simp_rw [← Subtype.exists_set_subtype, biUnion_image]

Premises used: Subtype.exists_set_subtype, Set.biUnion_image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
rcases :
  ∀ (T : Set (↑I : Type u_1)) (hTc : T.Countable)
    (hU : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s (↑i : ι)) (⋃ (i : (↑I : Type u_1)), s (↑i : ι))),
    ∃ (s_1 : Set (↑I : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
        Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)
⊢ ∃ (s_1 : Set (↑I : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
      Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)

Tactic:
rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩

Premises used: TopologicalSpace.isOpen_iUnion_countable, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
T : Set (↑I : Type u_1)
hTc : T.Countable
hU : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s (↑i : ι)) (⋃ (i : (↑I : Type u_1)), s (↑i : ι))
⊢ ∃ (s_1 : Set (↑I : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
      Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)

Tactic:
⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.iUnion_subtype, Eq.trans
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
T : Set (↑I : Type u_1)
hTc : T.Countable
hU : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s (↑i : ι)) (⋃ (i : (↑I : Type u_1)), s (↑i : ι))
⊢ ∃ (s_1 : Set (↑I : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
      Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)

Tactic:
exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
S : Set (Set α)
H : ∀ s ∈ S, IsOpen[t] s
⊢ ∃ (T : Set (Set α)), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Tactic:
simpa only [and_left_comm, sUnion_eq_biUnion] using isOpen_biUnion_countable S id H

Premises used: id, and_left_comm, Set.sUnion_eq_biUnion, TopologicalSpace.isOpen_biUnion_countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
rcases :
  ∀ (s : Set α) (hsc : s.Countable)
    (hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))),
    ∃ (s : Set α), s.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, f x) univ
⊢ ∃ (s : Set α), s.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, f x) univ

Tactic:
rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with
    ⟨s, hsc, hsU⟩

Premises used: TopologicalSpace.isOpen_iUnion_countable, isOpen_interior, interior
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))
suffices : Eq.{u + 1} (α := Set α) (⋃ x ∈ s, interior (f x)) univ
⊢ ∃ (s : Set α), s.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, f x) univ

Tactic:
suffices ⋃ x ∈ s, interior (f x) = univ from
    ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))
simp : ∀ (x : α), ∃ (i : α), x ∈ interior (f i)
⊢ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, interior (f x)) univ

Tactic:
simp only [hsU, eq_univ_iff_forall, mem_iUnion]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))
⊢ ∀ (x : α), ∃ (i : α), x ∈ interior (f i)

Tactic:
fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))
⊢ ∀ (x : α), ∃ (i : α), x ∈ interior (f i)

Tactic:
exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x

Tactic:
have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x
rcases :
  ∀ (t : Set (↑s : Type u)) (htc : t.Countable)
    (htU : Eq.{u + 1} (α := Set (↑s : Type u)) (⋃ x ∈ t, Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α)) univ),
    ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
rcases countable_cover_nhds this with ⟨t, htc, htU⟩

Premises used: TopologicalSpace.countable_cover_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htU : Eq.{u + 1} (α := Set (↑s : Type u)) (⋃ x ∈ t, Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α)) univ
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.image