awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
⊢ Function.RightInverse
    (fun (x : (↑s : Type u_1)) ↦
      Subtype.mk (p := fun (x : (↑(closure s) : Type u_1)) ↦
        Membership.mem (γ := Set (↑(closure s) : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) x)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ closure s) (↑x : X) ⋯) ⋯)
    fun (x : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ s) (↑(↑x : (↑(closure s) : Type u_1)) : X) ⋯

Tactic:
grind
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
⊢ Continuous.{u_1, u_1} (X := (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1))
    (Equiv.toFun
      {
        toFun := fun (x : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)) ↦
          Subtype.mk (p := fun (x : X) ↦ x ∈ s) (↑(↑x : (↑(closure s) : Type u_1)) : X) ⋯,
        invFun := fun (x : (↑s : Type u_1)) ↦
          Subtype.mk (p := fun (x : (↑(closure s) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(closure s) : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s)
              x)
            (Subtype.mk (p := fun (x : X) ↦ x ∈ closure s) (↑x : X) ⋯) ⋯,
        left_inv := ⋯, right_inv := ⋯ })

Tactic:
fun_prop
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
⊢ Continuous.{u_1, u_1} (X := (↑s : Type u_1)) (Y :=
    (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1))
    (Equiv.invFun
      {
        toFun := fun (x : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)) ↦
          Subtype.mk (p := fun (x : X) ↦ x ∈ s) (↑(↑x : (↑(closure s) : Type u_1)) : X) ⋯,
        invFun := fun (x : (↑s : Type u_1)) ↦
          Subtype.mk (p := fun (x : (↑(closure s) : Type u_1)) ↦
            Membership.mem (γ := Set (↑(closure s) : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s)
              x)
            (Subtype.mk (p := fun (x : X) ↦ x ∈ closure s) (↑x : X) ⋯) ⋯,
        left_inv := ⋯, right_inv := ⋯ })

Tactic:
fun_prop
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
have :
  ∀ (h_homeo : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1) ≃ₜ (↑s : Type u_1)),
    BaireSpace.{u_1} (↑s : Type u_1)
⊢ BaireSpace.{u_1} (↑s : Type u_1)

Tactic:
have h_homeo : Homeomorph ((↑) ⁻¹' s : Set (closure s)) s := ⟨⟨fun x => ⟨x, x.2⟩,
    fun x => ⟨⟨x, subset_closure x.2⟩, x.2⟩, by grind, by grind⟩, by fun_prop, by fun_prop⟩
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
h_homeo : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1) ≃ₜ (↑s : Type u_1)
⊢ BaireSpace.{u_1} (↑s : Type u_1)

Tactic:
h_homeo.baireSpace

Premises used: Homeomorph.baireSpace
-- Module: Mathlib.Topology.Baire.LocallyCompactRegular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : R1Space X
inst_2 : LocallyCompactSpace X
hG : IsGδ s
this_1 : BaireSpace.{u_1} (↑(closure s) : Type u_1)
this : BaireSpace.{u_1} (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1)
h_homeo : (↑(Subtype.val (p := fun (x : X) ↦ x ∈ closure s) ⁻¹' s) : Type u_1) ≃ₜ (↑s : Type u_1)
⊢ BaireSpace.{u_1} (↑s : Type u_1)

Tactic:
exact h_homeo.baireSpace

Premises used: Homeomorph.baireSpace
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
subst : IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})

Tactic:
subst t
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})

Tactic:
⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, le_generateFrom, TopologicalSpace.IsTopologicalBasis.mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
refine_1 :
  ∀ (t₁ : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₁ →
      ∀ (t₂ : Set α),
        Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₂ →
          ∀ x ∈ t₁ ∩ t₂,
            ∃ (t₃ : Set α),
              Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})
                  t₃ ∧
                x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
refine_2 : Eq.{u + 1} (α := Set α) (⋃₀ ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})) univ
refine_3 :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) s_1 →
      IsOpen[generateFrom s] s_1
refine_4 :
  ∀ (t : Set α) (ht : t ∈ s),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})

Tactic:
refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : t₁.Finite
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : t₂.Finite
ht₂b : t₂ ⊆ s
x : α
h : Membership.mem (γ := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) t₁ ∩ (fun (f : Set (Set α)) ↦ ⋂₀ f) t₂) x
⊢ ∃ (t₃ : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₃ ∧
      x ∈ t₃ ∧ t₃ ⊆ (fun (f : Set (Set α)) ↦ ⋂₀ f) t₁ ∩ (fun (f : Set (Set α)) ↦ ⋂₀ f) t₂

Tactic:
⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩

Premises used: Set.Finite.union, Set.sInter_union, Set.union_subset, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : t₁.Finite
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : t₂.Finite
ht₂b : t₂ ⊆ s
x : α
h : Membership.mem (γ := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) t₁ ∩ (fun (f : Set (Set α)) ↦ ⋂₀ f) t₂) x
⊢ ∃ (t₃ : Set α),
    Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t₃ ∧
      x ∈ t₃ ∧ t₃ ⊆ (fun (f : Set (Set α)) ↦ ⋂₀ f) t₁ ∩ (fun (f : Set (Set α)) ↦ ⋂₀ f) t₂

Tactic:
exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
refine_2 :
  ∀ (a : α),
    ∃ (i : Set (Set α)) (_ : Membership.mem (γ := Set (Set (Set α))) {f : Set (Set α) | f.Finite ∧ f ⊆ s} i), a ∈ ⋂₀ i
⊢ Eq.{u + 1} (α := Set α) (⋃₀ ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})) univ

Tactic:
rw [sUnion_image, iUnion₂_eq_univ_iff]

Premises used: Set.sUnion_image, Set.iUnion₂_eq_univ_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α),
    ∃ (i : Set (Set α)) (_ : Membership.mem (γ := Set (Set (Set α))) {f : Set (Set α) | f.Finite ∧ f ⊆ s} i), a ∈ ⋂₀ i

Tactic:
fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩

Premises used: Set.finite_empty, Set.sInter_empty, And.intro, Set.empty_subset, Exists.intro, Eq.substr, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α),
    ∃ (i : Set (Set α)) (_ : Membership.mem (γ := Set (Set (Set α))) {f : Set (Set α) | f.Finite ∧ f ⊆ s} i), a ∈ ⋂₀ i

Tactic:
exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : t.Finite
htb : t ⊆ s
⊢ IsOpen[generateFrom s] ((fun (f : Set (Set α)) ↦ ⋂₀ f) t)

Tactic:
hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs

Premises used: TopologicalSpace.GenerateOpen.basic, Set.Finite.isOpen_sInter
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : t.Finite
htb : t ⊆ s
⊢ IsOpen[generateFrom s] ((fun (f : Set (Set α)) ↦ ⋂₀ f) t)

Tactic:
exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs

Premises used: TopologicalSpace.GenerateOpen.basic, Set.Finite.isOpen_sInter
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
refine_4 :
  Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) (⋂₀ {t})
⊢ Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) t

Tactic:
rw [← sInter_singleton t]

Premises used: Set.sInter_singleton
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) (⋂₀ {t})

Tactic:
⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Mem, setOf, And.intro, Exists.intro, Set.image, Singleton.singleton, Set.finite_singleton, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ Membership.mem (γ := Set (Set α)) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}) (⋂₀ {t})

Tactic:
exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ IsTopologicalBasis.{u} (α := α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})

Tactic:
isTopologicalBasis_of_subbasis hsg

Premises used: TopologicalSpace.isTopologicalBasis_of_subbasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
h : s = (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}
⊢ IsTopologicalBasis s

Tactic:
convert! isTopologicalBasis_of_subbasis hsg

Premises used: TopologicalSpace.isTopologicalBasis_of_subbasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
s : Set (Set α)
hsg : t_1 = generateFrom s
hsi : FiniteInter s
t : Set α
ht : t ∈ s
⊢ Membership.mem (γ := Set (Set (Set α))) {f : Set (Set α) | f.Finite ∧ f ⊆ s} {t} ∧
    (fun (f : Set (Set α)) ↦ ⋂₀ f) {t} = t

Tactic:
simpa using ht
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
h : (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s} ≤ s
⊢ s = (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s}

Tactic:
refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Set (Set α)
hg : g.Finite
hgs : g ⊆ s
⊢ g.Finite

Tactic:
hg
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Set (Set α)
hg : g.Finite
hgs : g ⊆ s
h : ∀ (g : Finset (Set α)) (hgs : (↑g : Set (Set α)) ⊆ s), (fun (f : Set (Set α)) ↦ ⋂₀ f) (↑g : Set (Set α)) ∈ s
⊢ (fun (f : Set (Set α)) ↦ ⋂₀ f) g ∈ s

Tactic:
lift g to Finset (Set α) using hg

Premises used: Finset, Set
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Finset (Set α)
hgs : (↑g : Set (Set α)) ⊆ s
⊢ (fun (f : Set (Set α)) ↦ ⋂₀ f) (↑g : Set (Set α)) ∈ s

Tactic:
hsi.finiteInter_mem g hgs

Premises used: Set.Mem, FiniteInter.finiteInter_mem
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Finset (Set α)
hgs : (↑g : Set (Set α)) ⊆ s
⊢ (fun (f : Set (Set α)) ↦ ⋂₀ f) (↑g : Set (Set α)) ∈ s

Tactic:
exact hsi.finiteInter_mem g hgs

Premises used: FiniteInter.finiteInter_mem
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
r : Set (Set α)
hsg : t = generateFrom r
hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r
⊢ t = generateFrom (insert univ r)

Tactic:
simpa using hsg
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun (t : Set α) ↦ t ∈ s ∧ a ∈ t) id
t₁ : Set α
ht₁ : t₁ ∈ s
t₂ : Set α
ht₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simpa only [and_assoc, (h_nhds x).mem_iff]
      using (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))

Premises used: Filter.HasBasis.mem_iff, Filter.inter_mem, And.right, And.left, And.intro, and_assoc, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun (t : Set α) ↦ t ∈ s ∧ a ∈ t) id
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
simpa only [nhds_generateFrom, and_comm] using (h_nhds x).eq_biInf

Premises used: TopologicalSpace.nhds_generateFrom, Filter.HasBasis.eq_biInf, and_comm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ u ∈ s, IsOpen[t] u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u
a : α
⊢ ∀ (i : Set α), a ∈ i ∧ IsOpen[t] i → ∃ (i' : Set α), (i' ∈ s ∧ a ∈ i') ∧ id i' ⊆ i

Tactic:
simpa [and_assoc] using h_nhds a

Premises used: and_assoc
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
rw :
  Membership.mem (γ := Set (Set α))
      (⋃ (i : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} i), (𝓟 i).sets) s ↔
    ∃ t ∈ b, a ∈ t ∧ t ⊆ s
h : DirectedOn.{u} (α := Set α) (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) {s : Set α | a ∈ s ∧ s ∈ b}
ne : Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}
⊢ s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]

Premises used: Filter.biInf_sets_eq, TopologicalSpace.nhds_generateFrom, TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ Membership.mem (γ := Set (Set α))
      (⋃ (i : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} i), (𝓟 i).sets) s ↔
    ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
simp [and_assoc, and_left_comm]

Premises used: and_left_comm, and_assoc
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
a : α
s_1 : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
h :
  ∀ (u : Set α) (hu₁ : u ∈ b) (hu₂ : a ∈ u) (hu₃ : u ⊆ s ∩ t),
    ∃ (z : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} z ∧
        (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) t z
⊢ ∃ (z : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} z ∧
      (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) t z

Tactic:
let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
a : α
s_1 : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ (z : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} z ∧
      (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) t z

Tactic:
⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩

Premises used: Iff.mpr, Filter.le_principal_iff, HasSubset.Subset.trans, Set.inter_subset_left, And.intro, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
a : α
s_1 : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ (z : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ b} z ∧
      (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) s z ∧ (𝓟 ⁻¹'o fun (x1 x2 : Filter α) ↦ x1 ≥ x2) t z

Tactic:
exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
ne : ∀ (i : Set α) (h1 : i ∈ b) (h2 : a ∈ i), Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}
⊢ Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}

Tactic:
rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩

Premises used: Set.eq_univ_iff_forall, Iff.mp, TopologicalSpace.IsTopologicalBasis.sUnion_eq
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}

Tactic:
⟨i, h2, h1⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ Set.Nonempty.{u} (α := Set α) {s : Set α | a ∈ s ∧ s ∈ b}

Tactic:
exact ⟨i, h2, h1⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ IsOpen[t] s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

Premises used: isOpen_iff_mem_nhds, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s s' : Set (Set α)
h_open : ∀ u ∈ s', IsOpen[t] u
hs : IsTopologicalBasis s
hss' : s ⊆ s'
⊢ IsTopologicalBasis s'

Tactic:
isTopologicalBasis_of_isOpen_of_nhds h_open fun a _ ha u_open ↦
    have ⟨t, hts, ht⟩ := hs.isOpen_iff.mp u_open a ha; ⟨t, hss' hts, ht⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, Membership.mem, Exists, HasSubset.Subset, And, And.intro, Exists.intro, Iff.mp, _private.0.TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset.match_1
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
a : α
s : Set α
⊢ (∃ t ∈ b, a ∈ t ∧ t ⊆ s) ↔ ∃ (i : Set α), (i ∈ b ∧ a ∈ i) ∧ i ⊆ s

Tactic:
simp only [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
rw : IsOpen[generateFrom b] s
⊢ IsOpen[t] s

Tactic:
rw [hb.eq_generateFrom]

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[generateFrom b] s

Tactic:
.basic s hs

Premises used: TopologicalSpace.GenerateOpen.basic, IsOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[generateFrom b] s

Tactic:
exact .basic s hs
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsOpen[t] ∅

Tactic:
isOpen_empty

Premises used: isOpen_empty
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
u : Set α
hu : u ∈ s
⊢ IsOpen[t] u

Tactic:
h.isOpen hu

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsOpen[t] ∅

Tactic:
exacts [isOpen_empty, h.isOpen hu]

Premises used: isOpen_empty
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsTopologicalBasis (s \ {∅})

Tactic:
isTopologicalBasis_of_isOpen_of_nhds (fun _ hu ↦ h.isOpen hu.1) fun a _ ha hu ↦
    have ⟨t, hts, ht⟩ := h.isOpen_iff.mp hu a ha
    ⟨t, ⟨hts, ne_of_mem_of_not_mem' ht.1 <| notMem_empty _⟩, ht⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, Membership.mem, Exists, HasSubset.Subset, SDiff.sdiff, And, And.left, And.intro, Exists.intro, Iff.mp, Set.notMem_empty, EmptyCollection.emptyCollection, Singleton.singleton, ne_of_mem_of_not_mem', _private.0.TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset.match_1
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
ha : a ∈ s
⊢ s ∈ 𝓝 a

Tactic:
(hb.isOpen hs).mem_nhds ha

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
a : α
u : Set α
au : a ∈ u
ou : IsOpen[t] u
⊢ ∃ v ∈ b, a ∈ v ∧ v ⊆ u

Tactic:
hb.mem_nhds_iff.1 <| IsOpen.mem_nhds ou au

Premises used: IsOpen.mem_nhds, Iff.mp, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis B'

Tactic:
isTopologicalBasis_of_isOpen_of_nhds h_open fun x u hx hu => ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B B' : Set (Set α)
hB : IsTopologicalBasis B
h_open : ∀ u ∈ B', IsOpen[t] u
h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u
refine : ∀ (x : α) (u : Set α) (hx : x ∈ u) (hu : IsOpen[t] u), ∃ v ∈ B', x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis B'

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds h_open fun x u hx hu => ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds