awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ (x : α) (hx : x ∈ s), Membership.mem (γ := Set α) (⋃ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x) x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩
-- 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
x : α
hx : x ∈ s
simp :
  ∀ (htU : ∀ (x : (↑s : Type u)), Membership.mem (γ := Set α) (⋃ i ∈ t, f (↑i : α)) (↑x : α)),
    Membership.mem (γ := Set α) (⋃ y ∈ t, f (↑y : α)) x
⊢ Membership.mem (γ := Set α) (⋃ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x) x

Tactic:
simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢

Premises used: Set.eq_univ_iff_forall, Set.preimage_iUnion, Set.biUnion_image, Set.mem_preimage
-- 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
x : α
hx : x ∈ s
htU : ∀ (x : (↑s : Type u)), Membership.mem (γ := Set α) (⋃ i ∈ t, f (↑i : α)) (↑x : α)
⊢ Membership.mem (γ := Set α) (⋃ y ∈ t, f (↑y : α)) x

Tactic:
htU ⟨x, hx⟩

Premises used: Set.Mem, Subtype.mk
-- 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
x : α
hx : x ∈ s
htU : ∀ (x : (↑s : Type u)), Membership.mem (γ := Set α) (⋃ i ∈ t, f (↑i : α)) (↑x : α)
⊢ Membership.mem (γ := Set α) (⋃ y ∈ t, f (↑y : α)) x

Tactic:
exact htU ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
⊢ ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u

Tactic:
have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u :=
    fun x hx ↦ ht.exists_subset_of_mem_open hx hu
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u
choose! :
  ∀ (a : (x : α) → Set α) (hat : ∀ x ∈ u, a x ∈ t) (xa : ∀ x ∈ u, x ∈ a x) (au : ∀ x ∈ u, a x ⊆ u),
    ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
choose! a hat xa au using A
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
apply : ∀ (i : (↑u : Type u)), IsOpen[t_1] (a (↑i : α))
⊢ ∃ (T : Set (↑u : Type u)),
    T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))

Tactic:
apply isOpen_iUnion_countable _

Premises used: TopologicalSpace.isOpen_iUnion_countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
x : α
hx : x ∈ u
⊢ IsOpen[t_1] (a (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ u) x hx) : α))

Tactic:
ht.isOpen (hat x hx)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
x : α
hx : x ∈ u
⊢ IsOpen[t_1] (a (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ u) x hx) : α))

Tactic:
exact ht.isOpen (hat x hx)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
obtain :
  ∀ (T : Set (↑u : Type u)) (T_count : T.Countable)
    (hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))),
    ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
obtain ⟨T, T_count, hT⟩ : ∃ T : Set u, T.Countable ∧ ⋃ i ∈ T, a i = ⋃ (i : u), a i := by
    apply isOpen_iUnion_countable _
    rintro ⟨x, hx⟩
    exact ht.isOpen (hat x hx)

Premises used: Set.Elem, Set
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.image, Subtype.val
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_1 : (fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T ⊆ t
refine_2 :
  u = ⋃ (a_1 : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) ((fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T) a_1), a_1
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_1 : T ⊆ (fun (x : (↑u : Type u)) ↦ a (↑x : α)) ⁻¹' t
⊢ (fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T ⊆ t

Tactic:
simp only [image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
x : α
xu : x ∈ u
⊢ Membership.mem (γ := Set (↑u : Type u)) ((fun (x : (↑u : Type u)) ↦ a (↑x : α)) ⁻¹' t)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ u) x xu)

Tactic:
hat x xu

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
x : α
xu : x ∈ u
⊢ Membership.mem (γ := Set (↑u : Type u)) ((fun (x : (↑u : Type u)) ↦ a (↑x : α)) ⁻¹' t)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ u) x xu)

Tactic:
exact hat x xu
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_2 : u = ⋃ (i : (↑u : Type u)), a (↑i : α)
⊢ u = ⋃ (a_1 : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) ((fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T) a_1), a_1

Tactic:
rw [biUnion_image, hT]

Premises used: Set.biUnion_image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_2 : u ⊆ ⋃ (i : (↑u : Type u)), a (↑i : α)
refine_2₁ : ⋃ (i : (↑u : Type u)), a (↑i : α) ⊆ u
⊢ u = ⋃ (i : (↑u : Type u)), a (↑i : α)

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
x : α
hx : x ∈ u
refine_2 : ∃ i ∈ u, x ∈ a i
⊢ Membership.mem (γ := Set α) (⋃ (i : (↑u : Type u)), a (↑i : α)) x

Tactic:
simp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
x : α
hx : x ∈ u
⊢ ∃ i ∈ u, x ∈ a i

Tactic:
grind
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_2 : ∀ (i : α) (i_1 : i ∈ u), a i ⊆ u
⊢ ⋃ (i : (↑u : Type u)), a (↑i : α) ⊆ u

Tactic:
simp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
⊢ ∀ (i : α) (i_1 : i ∈ u), a i ⊆ u

Tactic:
grind
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
⊢ ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a

Tactic:
have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
    fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
choose! :
  ∀ (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),
    ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s

Tactic:
choose! s hst s_count hs using A
-- 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
⊢ ⋃ u ∈ countableBasis α, s u ⊆ t

Tactic:
simpa using hst
-- 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
refine : IsTopologicalBasis.{u} (α := α) (⋃ u ∈ countableBasis α, s u)
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s

Tactic:
refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst,
    (countable_countableBasis α).biUnion s_count, ?_⟩
-- 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
h_open : ∀ (u : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) u → IsOpen[t_1] u
h_nhds :
  ∀ (a : α) (u : Set α),
    a ∈ u →
      IsOpen[t_1] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) v ∧ a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u} (α := α) (⋃ u ∈ countableBasis α, s u)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- 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
h_open : ∀ (u x : Set α), x ∈ countableBasis α → u ∈ s x → IsOpen[t_1] u
⊢ ∀ (u : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) u → IsOpen[t_1] u

Tactic:
simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_iUnion, forall_exists_index, exists_prop
-- 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
⊢ ∀ (s : Set α) (hs : s ∈ t), IsOpen[t_1] s

Tactic:
have := @ht.isOpen
-- 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
this : ∀ (s : Set α) (hs : s ∈ t), IsOpen[t_1] s
⊢ ∀ (u x : Set α), x ∈ countableBasis α → u ∈ s x → IsOpen[t_1] u

Tactic:
grind
-- 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
h_nhds : ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
⊢ ∃ (v_1 : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) v_1 ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
simp only [mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- 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 ∈ countableBasis α, x ∈ u ∧ u ⊆ v

Tactic:
(isBasis_countableBasis α).isOpen_iff.1 hv _ hx

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, Iff.mp, TopologicalSpace.isBasis_countableBasis
-- 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
h_nhds :
  ∀ (u : Set α) (u_mem : u ∈ countableBasis α) (xu : x ∈ u) (uv : u ⊆ v),
    ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, TopologicalSpace.countableBasis, Iff.mp, TopologicalSpace.isBasis_countableBasis
-- 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
⊢ x ∈ u

Tactic:
xu
-- 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
h : ⋃ a ∈ s u, a = u
⊢ Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x

Tactic:
convert! xu
-- 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
⊢ ⋃ a ∈ s u, a = u

Tactic:
(hs u u_mem).symm

Premises used: Eq.symm
-- 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
⊢ ⋃ a ∈ s u, a = u

Tactic:
exact (hs u u_mem).symm

Premises used: Eq.symm
-- 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
⊢ Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x

Tactic:
have : x ∈ ⋃ a ∈ s u, a := by
      convert! xu
      exact (hs u u_mem).symm
-- 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 ∈ s u, x ∈ w

Tactic:
simpa using this
-- 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
h_nhds :
  ∀ (w : Set α) (ws : w ∈ s u) (xw : x ∈ w), ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
-- 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
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
h_nhds : w ⊆ v
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v

Tactic:
refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
-- 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
apply : w ⊆ ⋃ a ∈ s u, a
⊢ w ⊆ v

Tactic:
apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv

Premises used: Set.Subset.trans, Eq.subset, Eq.symm
-- 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:
subset_iUnion₂_of_subset w ws (Subset.refl _)

Premises used: Set.Subset.refl, Set.subset_iUnion₂_of_subset