awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t_1] cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure[inst] ct
⊢ s ×ˢ t ⊆ closure[t_1] cs ×ˢ closure[inst] ct

Tactic:
gcongr
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous[t, inst] f
rcases : ∀ (c : Set α) (c_count : c.Countable) (hc : s ⊆ closure[t] c), IsSeparable (f '' s)
⊢ IsSeparable (f '' s)

Tactic:
rcases hs with ⟨c, c_count, hc⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ IsSeparable (f '' s)

Tactic:
⟨f '' c, c_count.image _, ?_⟩

Premises used: TopologicalSpace.IsSeparable, Set.Countable.image, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
refine : f '' s ⊆ closure[inst] (f '' c)
⊢ IsSeparable (f '' s)

Tactic:
refine ⟨f '' c, c_count.image _, ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
rw : s ⊆ f ⁻¹' closure[inst] (f '' c)
⊢ f '' s ⊆ closure[inst] (f '' c)

Tactic:
rw [image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ s ⊆ f ⁻¹' closure[inst] (f '' c)

Tactic:
hc.trans (closure_subset_preimage_closure_image hf)

Premises used: HasSubset.Subset.trans, closure_subset_preimage_closure_image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous[t, inst] f
c : Set α
c_count : c.Countable
hc : s ⊆ closure[t] c
⊢ s ⊆ f ⁻¹' closure[inst] (f '' c)

Tactic:
exact hc.trans (closure_subset_preimage_closure_image hf)

Premises used: HasSubset.Subset.trans, closure_subset_preimage_closure_image
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
simp_rw : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ SeparableSpace α
simp_rw₁ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ Dense s
simp_rw₂ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ closure[t] s = univ
simp_rw₃ : (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s : Set α), s.Countable ∧ univ ⊆ closure[t] s
simp_rw₄ :
  (∃ (c : Set α), c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ (s_1 : Set α), s_1.Countable ∧ closure[t] s ⊆ closure[t] s_1
⊢ IsSeparable s ↔ SeparableSpace α

Tactic:
simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]

Premises used: Set.univ_subset_iff, TopologicalSpace.IsSeparable, dense_iff_closure_eq, Dense.closure_eq, IsClosed.closure_subset_iff, isClosed_closure, TopologicalSpace.separableSpace_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
⊢ IsSeparable.{u} (α := α) univ ↔ SeparableSpace α

Tactic:
dense_univ.isSeparable_iff

Premises used: dense_univ, Dense.isSeparable_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
f : α → β
hf : Continuous[t, inst] f
⊢ IsSeparable (range f)

Tactic:
image_univ (f := f) ▸ (isSeparable_univ_iff.2 ‹_›).image hf

Premises used: Iff.mpr, Set.image_univ, Eq.rec, TopologicalSpace.IsSeparable.image, TopologicalSpace.isSeparable_univ_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
inst : SeparableSpace.{u} (↑s : Type u)
⊢ IsSeparable s

Tactic:
simpa using isSeparable_range (continuous_subtype_val (p := (· ∈ s)))

Premises used: continuous_subtype_val, TopologicalSpace.isSeparable_range
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
s : Set α
⊢ IsSeparable s

Tactic:
IsSeparable.mono (isSeparable_univ_iff.2 h) (subset_univ _)

Premises used: Iff.mpr, Set.subset_univ, TopologicalSpace.IsSeparable.mono, TopologicalSpace.isSeparable_univ_iff
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}

Tactic:
isTopologicalBasis_of_isOpen_of_nhds ?_ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
refine_1 :
  ∀ (u : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} u →
      IsOpen[⨅ (i : ι), t i] u
refine_2 :
  ∀ (a : β) (u : Set β),
    a ∈ u →
      IsOpen[⨅ (i : ι), t i] u →
        ∃ (v : Set β),
          Membership.mem (γ := Set (Set β))
              {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
            a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
U : ι → Set β
F : Finset ι
hU : ∀ i ∈ F, U i ∈ T i
⊢ IsOpen[⨅ (i : ι), t i] (⋂ i ∈ F, U i)

Tactic:
isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, isOpen_biInter_finset, iInf_le, IsOpen.mono
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
U : ι → Set β
F : Finset ι
hU : ∀ i ∈ F, U i ∈ T i
⊢ IsOpen[⨅ (i : ι), t i] (⋂ i ∈ F, U i)

Tactic:
refine isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, isOpen_biInter_finset, iInf_le, IsOpen.mono
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
refine_2 :
  ∀ (F : Set ι) (U : (i : ι) → Set β) (hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u) (hF : (F, U).1.Finite)
    (hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i),
    ∃ (v : Set β),
      Membership.mem (γ := Set (Set β))
          {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
        a ∈ v ∧ v ⊆ u
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u

Tactic:
rcases (nhds_iInf (t := t) (a := a)).symm ▸ HasBasis.iInf'
      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u

Tactic:
⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩

Premises used: Set.Finite.toFinset, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
refine_2 : ∀ i ∈ hF.toFinset (s := (F, U).1), U i ∈ T i
refine_2₁ : Membership.mem (γ := Set β) (⋂ i ∈ hF.toFinset (s := (F, U).1), U i) a
refine_2₂ : ⋂ i ∈ hF.toFinset (s := (F, U).1), U i ⊆ u
⊢ ∃ (v : Set β),
    Membership.mem (γ := Set (Set β))
        {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i} v ∧
      a ∈ v ∧ v ⊆ u

Tactic:
refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
refine_2 : ∀ i ∈ F, U i ∈ T i
⊢ ∀ i ∈ hF.toFinset (s := (F, U).1), U i ∈ T i

Tactic:
simp only [Finite.mem_toFinset, mem_iInter]

Premises used: Set.Finite.mem_toFinset, Set.mem_iInter
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
refine_2 : ∀ (i : ι) (i_1 : i ∈ F), a ∈ U i
⊢ Membership.mem (γ := Set β) (⋂ i ∈ hF.toFinset (s := (F, U).1), U i) a

Tactic:
simp only [Finite.mem_toFinset, mem_iInter]

Premises used: Set.Finite.mem_toFinset, Set.mem_iInter
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
refine_2 : ⋂ i ∈ F, U i ⊆ u
⊢ ⋂ i ∈ hF.toFinset (s := (F, U).1), U i ⊆ u

Tactic:
simp only [Finite.mem_toFinset, mem_iInter]

Premises used: Set.Finite.mem_toFinset, Set.mem_iInter
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, U i ∈ T i

Tactic:
fun i hi ↦ (hU i hi).1

Premises used: Set.Mem, And.left
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ i ∈ F, U i ∈ T i

Tactic:
exact fun i hi ↦ (hU i hi).1

Premises used: And.left
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ (i : ι) (i_1 : i ∈ F), a ∈ U i

Tactic:
fun i hi ↦ (hU i hi).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ∀ (i : ι) (i_1 : i ∈ F), a ∈ U i

Tactic:
exact fun i hi ↦ (hU i hi).2

Premises used: And.right
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u

Tactic:
hUu

Premises used: Set.Mem
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x : TopologicalSpace β := ⨅ (i : ι), t i
a : β
u : Set β
ha : a ∈ u
hu : IsOpen[⨅ (i : ι), t i] u
F : Set ι
U : (i : ι) → Set β
hUu : ⋂ i ∈ (F, U).1, (F, U).2 i ⊆ u
hF : (F, U).1.Finite
hU : ∀ i ∈ (F, U).1, (F, U).2 i ∈ T i ∧ a ∈ (F, U).2 i
⊢ ⋂ i ∈ F, U i ⊆ u

Tactic:
exact hUu
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i}

Tactic:
IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i))

Premises used: IsTopologicalBasis.iInf, TopologicalSpace.IsTopologicalBasis.induced
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
h :
  ∀ (S : Set β),
    (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
      ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
⊢ IsTopologicalBasis.{u_1} (α := β)
    {S : Set β | ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}

Tactic:
convert! IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S

Premises used: IsTopologicalBasis.iInf, TopologicalSpace.IsTopologicalBasis.induced
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
h :
  (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
    ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
h₁ :
  (∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i) →
    ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ (∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
constructor
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩

Premises used: Set.preimage, Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : (i : ι) → Set (X i)
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ T i
hSU : S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hUT : ∀ i ∈ F, U i ∈ preimage (f i) '' T i
hSU : S = ⋂ i ∈ F, U i
h :
  ∀ (U' : (i : ι) → Set (X i)) (hU' : ∀ i ∈ F, U' i ∈ T i) (hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i),
    ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
⊢ ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
choose! U' hU' hUU' using hUT
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hSU : S = ⋂ i ∈ F, U i
U' : (i : ι) → Set (X i)
hU' : ∀ i ∈ F, U' i ∈ T i
hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i
⊢ ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

Premises used: Eq.rec, And.intro, Exists.intro, Set.iInter₂_congr, Eq.symm
-- Module: Mathlib.Topology.Bases
Goal:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
U : ι → Set β
F : Finset ι
hSU : S = ⋂ i ∈ F, U i
U' : (i : ι) → Set (X i)
hU' : ∀ i ∈ F, U' i ∈ T i
hUU' : ∀ i ∈ F, f i ⁻¹' U' i = U i
⊢ ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i

Tactic:
exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis (α := (i : ι) → X i)
    {S : Set ((i : ι) → X i) |
      ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F : Set ι).pi (α := X) U}

Tactic:
simpa only [Set.pi_def] using IsTopologicalBasis.iInf_induced cond eval

Premises used: Function.eval, Set.pi_def, IsTopologicalBasis.iInf_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
⊢ IsTopologicalBasis.{u_1} (α := α) {s : Set α | ∃ (x : α), s = {x}}

Tactic:
isTopologicalBasis_of_isOpen_of_nhds (fun _ _ => isOpen_discrete _) fun x _ hx _ =>
    ⟨{x}, ⟨x, rfl⟩, mem_singleton x, singleton_subset_iff.2 hx⟩

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, And.intro, isOpen_discrete, Exists.intro, Singleton.singleton, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
h : IsTopologicalBasis B
p : α → Prop
⊢ IsTopologicalBasis (α := Subtype p) (preimage (Subtype.val (p := p)) '' B)

Tactic:
h.isInducing ⟨rfl⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isInducing, Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)

Tactic:
(isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_

Premises used: Iff.mpr, TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, TopologicalSpace.isTopologicalBasis_opens, isTopologicalBasis_pi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)

Tactic:
refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_

Premises used: Iff.mpr, TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, TopologicalSpace.isTopologicalBasis_opens, isTopologicalBasis_pi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
inl : ∀ (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inr : ∀ (h : ((↑s : Set ι).pi (α := X) U).Nonempty), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)

Tactic:
obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, SetLike.coe, Set.pi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
U : (i : ι) → Set (X i)
s : Finset ι
hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)
h : (↑s : Set ι).pi (α := X) U = ∅
⊢ IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)

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

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

Tactic:
rw [eval_image_pi (mod_cast hi) h]

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

Tactic:
hU _ hi

Premises used: Set.Mem, setOf, IsOpen