awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
obtain : ∀ (w : Set α) (hwB : w ∈ B) (hxw : x ∈ w) (hwu : w ⊆ u), ∃ v ∈ B', x ∈ v ∧ v ⊆ u
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨w, hwB, hxw, hwu⟩ := hB.exists_subset_of_mem_open hx hu

Premises used: TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
obtain : ∀ (v : Set α) (hvB' : v ∈ B') (hxv : x ∈ v) (hvw : v ⊆ w), ∃ v ∈ B', x ∈ v ∧ v ⊆ u
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, hvB', hxv, hvw⟩ := h w hwB x hxw
-- 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
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
v : Set α
hvB' : v ∈ B'
hxv : x ∈ v
hvw : v ⊆ w
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u

Tactic:
⟨v, hvB', hxv, hvw.trans hwu⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- 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
x : α
u : Set α
hx : x ∈ u
hu : IsOpen[t] u
w : Set α
hwB : w ∈ B
hxw : x ∈ w
hwu : w ⊆ u
v : Set α
hvB' : v ∈ B'
hxv : x ∈ v
hvw : v ⊆ w
⊢ ∃ v ∈ B', x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨v, hvB', hxv, hvw.trans hwu⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃₀ {s : Set α | s ∈ B ∧ s ⊆ u}

Tactic:
ext fun _a =>
    ⟨fun ha =>
      let ⟨b, hb, ab, bu⟩ := hB.exists_subset_of_mem_open ha ou
      ⟨b, ⟨hb, bu⟩, ab⟩,
      fun ⟨_b, ⟨_, bu⟩, ab⟩ => bu ab⟩

Premises used: Set.ext, _private.0.TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'.match_2, setOf, Set.sUnion, Membership.mem, HasSubset.Subset, And, And.intro, Iff.intro, Exists.intro, _private.0.TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'.match_1, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ ∃ S ⊆ B, u = ⋃₀ S

Tactic:
⟨{ s ∈ B | s ⊆ u }, fun _ h => h.1, hB.open_eq_sUnion' ou⟩

Premises used: setOf, Membership.mem, HasSubset.Subset, And, And.left, And.intro, Exists.intro, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
⊢ IsOpen[t] u ↔ ∃ S ⊆ B, u = ⋃₀ S

Tactic:
⟨hB.open_eq_sUnion, fun ⟨_S, hSB, hu⟩ => hu.symm ▸ isOpen_sUnion fun _s hs => hB.isOpen (hSB hs)⟩

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, TopologicalSpace.IsTopologicalBasis.isOpen, Eq.rec, _private.0.TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion.match_1, Iff.intro, IsOpen, isOpen_sUnion, Eq.symm
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
rw : u = ⋃₀ {s : Set α | s ∈ B ∧ s ⊆ u}
⊢ u = ⋃ (i : (↑{s : Set α | s ∈ B ∧ s ⊆ u} : Type u)), (↑i : Set α)

Tactic:
rw [← sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen[t] u
⊢ u = ⋃₀ {s : Set α | s ∈ B ∧ s ⊆ u}

Tactic:
apply hB.open_eq_sUnion' ou

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
s : Set α
hs : IsOpen[t] s
obtain : ∀ (S : Set (Set α)) (hS : S ⊆ B) (hs : IsOpen[t] (⋃₀ S)), P (⋃₀ S)
⊢ P s

Tactic:
obtain ⟨S, hS, rfl⟩ := hB.open_eq_sUnion hs

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
S : Set (Set α)
hS : S ⊆ B
hs : IsOpen[t] (⋃₀ S)
⊢ P (⋃₀ S)

Tactic:
sUnion _ fun b hb ↦ basis _ <| hS hb
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
P : Set α → Prop
hB : IsTopologicalBasis B
basis : ∀ b ∈ B, P b
sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)
S : Set (Set α)
hS : S ⊆ B
hs : IsOpen[t] (⋃₀ S)
⊢ P (⋃₀ S)

Tactic:
exact sUnion _ fun b hb ↦ basis _ <| hS hb
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
rw : ⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t
⊢ s ⊆ t

Tactic:
rw [hB.open_eq_sUnion' hs]

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ ⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t

Tactic:
simpa [sUnion_subset_iff]

Premises used: Set.sUnion_subset_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
ht : IsOpen[t_1] t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
rw : Eq.{u + 1} (α := Set α) (⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s}) (⋃₀ {s : Set α | s ∈ B ∧ s ⊆ t})
⊢ s = t

Tactic:
rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
ht : IsOpen[t_1] t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ Eq.{u + 1} (α := Set α) (⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s}) (⋃₀ {s : Set α | s ∈ B ∧ s ⊆ t})

Tactic:
congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

Premises used: Set.ext, and_congr_right, congr_arg
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t_1] s
ht : IsOpen[t_1] t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ Eq.{u + 1} (α := Set α) (⋃₀ {s_1 : Set α | s_1 ∈ B ∧ s_1 ⊆ s}) (⋃₀ {s : Set α | s ∈ B ∧ s ⊆ t})

Tactic:
exact congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

Premises used: Set.ext, and_congr_right, congr_arg
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
a : α
⊢ (∀ (i : Set α), i ∈ b ∧ a ∈ i → (i ∩ s).Nonempty) ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty

Tactic:
simp only [and_imp]

Premises used: and_imp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
simp : (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
⊢ Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
simp only [Dense, hb.mem_closure_iff]

Premises used: Dense, TopologicalSpace.IsTopologicalBasis.mem_closure_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩

Premises used: Inter.inter, Set.Nonempty, _private.0.TopologicalSpace.IsTopologicalBasis.dense_iff.match_1, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty

Tactic:
exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
⊢ IsOpenMap f ↔ ∀ s ∈ B, IsOpen[inst] (f '' s)

Tactic:
⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, Iff.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
refine : ∀ (hf : ∀ s ∈ B, IsOpen[inst] (f '' s)) (o : Set α) (ho : IsOpen[t] o), IsOpen[inst] (f '' o)
⊢ IsOpenMap f ↔ ∀ s ∈ B, IsOpen[inst] (f '' s)

Tactic:
refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst] (f '' s)
o : Set α
ho : IsOpen[t] o
rw : IsOpen[inst] (⋃ (i : (↑{s : Set α | s ∈ B ∧ s ⊆ o} : Type u)), f '' (↑i : Set α))
⊢ IsOpen[inst] (f '' o)

Tactic:
rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]

Premises used: Set.sUnion_eq_iUnion, Set.image_iUnion, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst] (⋃ (i : (↑{s : Set α | s ∈ B ∧ s ⊆ o} : Type u)), f '' (↑i : Set α))

Tactic:
isOpen_iUnion fun s => hf s s.2.1

Premises used: isOpen_iUnion, And.left, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst] (⋃ (i : (↑{s : Set α | s ∈ B ∧ s ⊆ o} : Type u)), f '' (↑i : Set α))

Tactic:
exact isOpen_iUnion fun s => hf s s.2.1
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hb : IsTopologicalBasis B
u : Set α
hu : u.Nonempty
ou : IsOpen[t] u
⊢ ∃ v ∈ B, v.Nonempty ∧ v ⊆ u

Tactic:
let ⟨x, hx⟩ := hu
  let ⟨v, vB, xv, vu⟩ := hb.exists_subset_of_mem_open hx ou
  ⟨v, vB, ⟨x, xv⟩, vu⟩

Premises used: Membership.mem, Exists, HasSubset.Subset, And, Set.Nonempty, _private.0.TopologicalSpace.IsTopologicalBasis.dense_iff.match_1, And.intro, Exists.intro, _private.0.TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'.match_1, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
tauto tauto₁ tauto₂ : ∀ (u : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u → IsOpen[t] u
⊢ ∀ (u : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u → IsOpen[t] u

Tactic:
tauto
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u
h :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
w : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₁ :
  ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u ∧ a ∈ u ∧ u ⊆ u
w₁ : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₂ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u
h₃ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → a ∈ u ∧ u ⊆ u
w₂ : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₄ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} u
h₅ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → a ∈ u ∧ u ⊆ u
w₃ : (a : α) → (u : Set α) → a ∈ u → IsOpen[t] u → Set α
h₆ h₇ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[t] u → a ∈ u ∧ u ⊆ u
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[t] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[t] U} v ∧ a ∈ v ∧ v ⊆ u

Tactic:
tauto
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
⊢ (𝓝 a).HasBasis
    (fun (x : Set α) ↦ x ∈ image (α := Set β) (preimage f ∘ fun (t : Set β) ↦ t) {i : Set β | i ∈ T ∧ f a ∈ i}) id

Tactic:
(hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id

Premises used: Topology.IsInducing.basis_nhds, Filter.HasBasis.to_image_id, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
h₁ :
  ∀ (s : Set α),
    s ∈ preimage f '' T ∧ a ∈ s ↔
      s ∈ image (α := Set β) (preimage f ∘ fun (t : Set β) ↦ t) {i : Set β | i ∈ T ∧ f a ∈ i}
⊢ (𝓝 a).HasBasis (fun (t : Set α) ↦ t ∈ preimage f '' T ∧ a ∈ t) id

Tactic:
convert! (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s

Premises used: Topology.IsInducing.basis_nhds, Filter.HasBasis.to_image_id, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : IsInducing f
h : IsTopologicalBasis T
a : α
s : Set α
⊢ s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ image (α := Set β) (preimage f ∘ fun (t : Set β) ↦ t) {i : Set β | i ∈ T ∧ f a ∈ i}

Tactic:
aesop
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
α : Type u_2
s : TopologicalSpace β
f : α → β
T : Set (Set β)
h : IsTopologicalBasis T
⊢ IsTopologicalBasis (preimage f '' T)

Tactic:
h.isInducing (t := induced f s) (.induced f)

Premises used: TopologicalSpace.IsTopologicalBasis.isInducing, Topology.IsInducing.induced
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (α := β) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂)

Tactic:
.of_hasBasis_nhds (t := ?_) fun a ↦ ?_

Premises used: TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
refine :
  ∀ (a : β),
    (𝓝 a).HasBasis
      (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id
⊢ IsTopologicalBasis (α := β) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂)

Tactic:
refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
rw :
  (𝓝 a ⊓ 𝓝 a).HasBasis
    (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id
⊢ (𝓝 a).HasBasis
    (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id

Tactic:
rw [nhds_inf (t₁ := t₁)]

Premises used: nhds_inf
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
⊢ (𝓝 a ⊓ 𝓝 a).HasBasis
    (fun (x : Set β) ↦
      Membership.mem (γ := Set (Set β))
        ((fun (i : Set β × Set β) ↦ i.1 ∩ i.2) '' {i : Set β × Set β | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}) x)
    id

Tactic:
((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id

Premises used: Filter.HasBasis.inf, Filter.HasBasis.to_image_id, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
h :
  ∀ (x : Set β),
    Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) x ∧ a ∈ x ↔
      Membership.mem (γ := Set (Set β))
        ((fun (i : Set β × Set β) ↦ i.1 ∩ i.2) '' {i : Set β × Set β | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}) x
⊢ (𝓝 a ⊓ 𝓝 a).HasBasis
    (fun (t : Set β) ↦ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) t ∧ a ∈ t) id

Tactic:
convert! ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id

Premises used: Filter.HasBasis.inf, Filter.HasBasis.to_image_id, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
t₁ t₂ : TopologicalSpace β
B₁ B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : β
x : Set β
⊢ Membership.mem (γ := Set (Set β)) (image2 (fun (x1 x2 : Set β) ↦ x1 ∩ x2) B₁ B₂) x ∧ a ∈ x ↔
    Membership.mem (γ := Set (Set β))
      ((fun (i : Set β × Set β) ↦ i.1 ∩ i.2) '' {i : Set β × Set β | (i.1 ∈ B₁ ∧ a ∈ i.1) ∧ i.2 ∈ B₂ ∧ a ∈ i.2}) x

Tactic:
aesop
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
γ : Type u_2
s : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
f₁ : γ → α
f₂ : γ → β
⊢ IsTopologicalBasis.{u_2} (α := γ) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)

Tactic:
simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)

Premises used: Set.image2_image_right, Set.image2_image_left, TopologicalSpace.IsTopologicalBasis.inf, TopologicalSpace.IsTopologicalBasis.induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (α := α × β) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) B₁ B₂)

Tactic:
h₁.inf_induced h₂ Prod.fst Prod.snd

Premises used: Set.Mem, setOf, TopologicalSpace.IsTopologicalBasis.inf_induced, Set.prod, Prod.fst, Set.preimage, Prod.snd
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ IsTopologicalBasis.{u} (α := α) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i)

Tactic:
isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
refine_1 :
  ∀ (u : Set α)
    (hu : Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) u),
    IsOpen[t] u
refine_2 :
  ∀ (a : α) (u : Set α),
    a ∈ u →
      IsOpen[t] u →
        ∃ (v : Set α),
          Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
            a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u} (α := α) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i)

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) u
⊢ ∃ (i : ι), ∃ x ∈ b i, Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' x = u

Tactic:
simp only [mem_iUnion, mem_image] at hu

Premises used: Set.mem_iUnion, Set.mem_image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : ∃ (i : ι), ∃ x ∈ b i, Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' x = u
refine_1 :
  ∀ (i : ι) (s : Set { x : α // x ∈ U i }) (sb : s ∈ b i), IsOpen[t] (Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' s)
⊢ IsOpen[t] u

Tactic:
rcases hu with ⟨i, s, sb, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x : α // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen[t] (Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' s)

Tactic:
(Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x : α // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen[t] (Subtype.val (p := fun (x : α) ↦ x ∈ U i) '' s)

Tactic:
exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, IsOpen.isOpenMap_subtype_val
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
refine_2 :
  ∀ (i : ι) (hi : a ∈ U i),
    ∃ (v : Set α),
      Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
        a ∈ v ∧ v ⊆ u
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      a ∈ v ∧ v ⊆ u

Tactic:
rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩

Premises used: Set.iUnion_eq_univ_iff, Iff.mp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
i : ι
hi : a ∈ U i
⊢ a ∈ U i

Tactic:
hi
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : Eq.{u + 1} (α := Set α) (⋃ (i : ι), U i) univ
b : (i : ι) → Set (Set (↑(U i) : Type u))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen[t] u
i : ι
hi : a ∈ U i
refine_2 :
  ∀ (a : { x : α // x ∈ U i }) (ha : (↑a : α) ∈ u),
    ∃ (v : Set α),
      Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
        (↑a : α) ∈ v ∧ v ⊆ u
⊢ ∃ (v : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ (i : ι), image (Subtype.val (p := fun (x : α) ↦ x ∈ U i)) '' b i) v ∧
      a ∈ v ∧ v ⊆ u

Tactic:
lift a to ↥(U i) using hi