awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
uo : IsOpen[t] u
i : ι
a : { x : α // x ∈ U i }
ha : (↑a : α) ∈ u
refine_2 :
  ∀ (v : Set (↑(U i) : Type u)) (hvb : v ∈ b i) (hav : a ∈ v)
    (hvu : v ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' 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:
rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
      ⟨v, hvb, hav, hvu⟩

Premises used: continuous_subtype_val, IsOpen.preimage, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 α
uo : IsOpen[t] u
i : ι
a : { x : α // x ∈ U i }
ha : (↑a : α) ∈ u
v : Set (↑(U i) : Type u)
hvb : v ∈ b i
hav : a ∈ v
hvu : v ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' 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:
⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
      image_subset_iff.2 hvu⟩

Premises used: Iff.mpr, Set.mem_iUnion, And.intro, Exists.intro, Set.image, Set.image_subset_iff
-- 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 α
uo : IsOpen[t] u
i : ι
a : { x : α // x ∈ U i }
ha : (↑a : α) ∈ u
v : Set (↑(U i) : Type u)
hvb : v ∈ b i
hav : a ∈ v
hvu : v ⊆ Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' 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:
exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
      image_subset_iff.2 hvu⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
rw : Continuous[t, generateFrom B] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
rw₁ rw₂ : (∀ s ∈ B, IsOpen[t] (f ⁻¹' s)) ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)
⊢ Continuous[t, inst] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)

Tactic:
rw [hB.eq_generateFrom, continuous_generateFrom_iff]

Premises used: TopologicalSpace.IsTopologicalBasis.eq_generateFrom, continuous_generateFrom_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
rw :
  (∀ (t_1 : Set β), IsOpen[inst] t_1 → ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) ↔
    ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
⊢ ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s

Tactic:
rw [continuousOn_iff']

Premises used: continuousOn_iff'
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ (∀ (t_1 : Set β), IsOpen[inst] t_1 → ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) ↔
    ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s

Tactic:
⟨fun h t ht => h t (hB.isOpen ht), fun h t ht => ?_⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, Iff.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
refine :
  ∀ (h : ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) (t_1 : Set β) (ht : IsOpen[inst] t_1),
    ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
⊢ (∀ (t_1 : Set β), IsOpen[inst] t_1 → ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) ↔
    ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s

Tactic:
refine ⟨fun h t ht => h t (hB.isOpen ht), fun h t ht => ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t ∈ B, ∃ (u : Set α), IsOpen[t_1] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst] t
obtain :
  ∀ (ι : Type u_1) (g : ι → Set β) (hg : ∀ (i : ι), g i ∈ B) (ht : IsOpen[inst] (⋃ (i : ι), g i)),
    ∃ (u : Set α), IsOpen[t_1] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s
⊢ ∃ (u : Set α), IsOpen[t_1] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
obtain ⟨ι, g, rfl, hg⟩ := hB.open_eq_iUnion ht

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_iUnion, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst] (⋃ (i : ι), g i)
choose :
  ∀ (v : (i : ι) → Set α) (hv : ∀ (i : ι), IsOpen[t] (v i)) (he : ∀ (i : ι), f ⁻¹' g i ∩ s = v i ∩ s),
    ∃ (u : Set α), IsOpen[t] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s
⊢ ∃ (u : Set α), IsOpen[t] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s

Tactic:
choose v hv he using (fun i => h (g i) (hg i))
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst] (⋃ (i : ι), g i)
v : (i : ι) → Set α
hv : ∀ (i : ι), IsOpen[t] (v i)
he : ∀ (i : ι), f ⁻¹' g i ∩ s = v i ∩ s
⊢ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = (⋃ (i : ι), v i) ∩ s

Tactic:
simp_all [iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst] (⋃ (i : ι), g i)
v : (i : ι) → Set α
hv : ∀ (i : ι), IsOpen[t] (v i)
he : ∀ (i : ι), f ⁻¹' g i ∩ s = v i ∩ s
⊢ ∃ (u : Set α), IsOpen[t] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s

Tactic:
exact ⟨⋃ i, v i, isOpen_iUnion hv, by simp_all [iUnion_inter]⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis.{u} (α := α) ∅
⊢ IsEmpty α

Tactic:
simpa using h.sUnion_eq.symm

Premises used: Eq.symm, TopologicalSpace.IsTopologicalBasis.sUnion_eq
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ (t₁ : Set α),
    Membership.mem (γ := Set (Set α)) ∅ t₁ →
      ∀ (t₂ : Set α),
        Membership.mem (γ := Set (Set α)) ∅ t₂ →
          ∀ x ∈ t₁ ∩ t₂, ∃ (t₃ : Set α), Membership.mem (γ := Set (Set α)) ∅ t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ Eq.{u + 1} (α := Set α) (⋃₀ ∅) univ

Tactic:
simp [Set.univ_eq_empty_iff.2]

Premises used: Iff.mpr, Set.univ_eq_empty_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : IsTopologicalBasis (α := α) {∅}
⊢ IsEmpty α

Tactic:
simpa using h.diff_empty

Premises used: TopologicalSpace.IsTopologicalBasis.diff_empty
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ∀ (t₁ : Set α),
    Membership.mem (γ := Set (Set α)) {∅} t₁ →
      ∀ (t₂ : Set α),
        Membership.mem (γ := Set (Set α)) {∅} t₂ →
          ∀ x ∈ t₁ ∩ t₂, ∃ (t₃ : Set α), Membership.mem (γ := Set (Set α)) {∅} t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
simp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ Eq (α := Set α) (⋃₀ {∅}) univ

Tactic:
simp [Set.univ_eq_empty_iff.2]

Premises used: Iff.mpr, Set.univ_eq_empty_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
⊢ ∃ (s : Set α), s.Countable ∧ Dense s

Tactic:
SeparableSpace.exists_countable_dense

Premises used: TopologicalSpace.SeparableSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
obtain : ∀ (s : Set α) (hs : s.Countable) (s_dense : Dense s), ∃ (u : ℕ → α), DenseRange u
⊢ ∃ (u : ℕ → α), DenseRange u

Tactic:
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α

Premises used: TopologicalSpace.exists_countable_dense, Set
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
obtain : ∀ (u : ℕ → α) (hu : s ⊆ range u), ∃ (u : ℕ → α), DenseRange u
⊢ ∃ (u : ℕ → α), DenseRange u

Tactic:
obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs

Premises used: Set.countable_iff_exists_subset_range, Iff.mp
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ (u : ℕ → α), DenseRange u

Tactic:
⟨u, s_dense.mono hu⟩

Premises used: Dense.mono, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ (u : ℕ → α), DenseRange u

Tactic:
exact ⟨u, s_dense.mono hu⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
⊢ DenseRange (denseSeq α)

Tactic:
Classical.choose_spec (exists_dense_seq α)

Premises used: Classical.choose_spec, TopologicalSpace.exists_dense_seq, TopologicalSpace.denseSeq
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_2
inst : Countable ι
u : ι → α
hu : DenseRange u
⊢ SeparableSpace α

Tactic:
⟨⟨range u, countable_range u, hu⟩⟩

Premises used: Set.countable_range, And.intro, Exists.intro, Set.range, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : TopologicalSpace β
f : α → β
h : DenseRange f
h' : Continuous[t, inst_1] f
⊢ SeparableSpace β

Tactic:
let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α
  ⟨⟨f '' s, Countable.image s_cnt f, h.dense_image h' s_dense⟩⟩

Premises used: Set.Countable.image, TopologicalSpace.exists_countable_dense, And.intro, Exists.intro, Set.image, TopologicalSpace.SeparableSpace.mk, DenseRange.dense_image, _private.0.DenseRange.separableSpace.match_1, TopologicalSpace.SeparableSpace
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsQuotientMap f
⊢ SeparableSpace β

Tactic:
hf.surjective.denseRange.separableSpace hf.continuous

Premises used: Topology.IsQuotientMap.surjective, Function.Surjective.denseRange, DenseRange.separableSpace, Topology.IsQuotientMap.continuous
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
inl : IsEmpty α → SeparableSpace α
inr : Nonempty α → SeparableSpace α
⊢ SeparableSpace α

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : IsEmpty α
⊢ SeparableSpace α

Tactic:
infer_instance
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
inr : ∀ (s : Set β) (s_cnt : s.Countable) (s_dense : Dense s), SeparableSpace α
⊢ SeparableSpace α

Tactic:
obtain ⟨s, s_cnt, s_dense⟩ := exists_countable_dense β

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ SeparableSpace α

Tactic:
⟨f.invFun '' s, s_cnt.image _, ?_⟩

Premises used: Function.invFun, Set.Countable.image, And.intro, Exists.intro, Set.image, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
inr : Dense (invFun f '' s)
⊢ SeparableSpace α

Tactic:
refine ⟨f.invFun '' s, s_cnt.image _, ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
inr : ∀ (x : α) (o : Set β), IsOpen[inst] o → f x ∈ o → (o ∩ f '' invFun f '' s).Nonempty
⊢ Dense (invFun f '' s)

Tactic:
simp_rw [h'.dense_iff, mem_closure_iff]

Premises used: mem_closure_iff, Topology.IsInducing.dense_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst] U
hx : f x ∈ U
inr : ∀ (x' : α) (hx's : f x' ∈ s) (hx'U : f x' ∈ U), (U ∩ f '' invFun f '' s).Nonempty
⊢ (U ∩ f '' invFun f '' s).Nonempty

Tactic:
obtain ⟨-, ⟨hx'U, x', rfl⟩, hx's⟩ :=
    s_dense.inter_open_nonempty (U ∩ range f) (hU.inter h.isOpen_range) ⟨f x, hx, mem_range_self _⟩

Premises used: Set.mem_range_self, Inter.inter, Dense.inter_open_nonempty, And.intro, IsOpen.inter, Exists.intro, Set.range, IsOpenMap.isOpen_range, rfl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U : f x' ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty

Tactic:
⟨f <| f.invFun <| f x', ?_, mem_image_of_mem _ <| mem_image_of_mem _ hx's⟩

Premises used: Function.invFun, Set.Nonempty, Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U : f x' ∈ U
inr : f (invFun f (f x')) ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty

Tactic:
refine ⟨f <| f.invFun <| f x', ?_, mem_image_of_mem _ <| mem_image_of_mem _ hx's⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U inr inr₁ inr₂ inr₃ : f x' ∈ U
⊢ f (invFun f (f x')) ∈ U

Tactic:
rwa [Function.apply_invFun_apply (f := f)]

Premises used: Function.apply_invFun_apply
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : Injective f
⊢ SeparableSpace α

Tactic:
let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense β
  ⟨f ⁻¹' s, s_cnt.preimage h', s_dense.preimage h⟩

Premises used: TopologicalSpace.exists_countable_dense, Set.preimage, And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk, Dense.preimage, Set.Countable.preimage, _private.0.DenseRange.separableSpace.match_1, TopologicalSpace.SeparableSpace
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenEmbedding f
⊢ SeparableSpace α

Tactic:
h.isOpenMap.separableSpace_of_injective h.injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Topology.IsEmbedding.injective, IsOpenMap.separableSpace_of_injective
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
rcases : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s), SeparableSpace (α × β)
⊢ SeparableSpace (α × β)

Tactic:
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
rcases : ∀ (t_1 : Set β) (htc : t_1.Countable) (htd : Dense t_1), SeparableSpace (α × β)
⊢ SeparableSpace (α × β)

Tactic:
rcases exists_countable_dense β with ⟨t, htc, htd⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ SeparableSpace (α × β)

Tactic:
⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩

Premises used: SProd.sprod, Set.Countable.prod, And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk, Dense.prod
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
⊢ SeparableSpace (α × β)

Tactic:
exact ⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
choose :
  ∀ (t : (x : ι) → Set (X x)) (htc : ∀ (x : ι), (t x).Countable) (htd : ∀ (x : ι), Dense (t x)),
    SeparableSpace ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
choose t htc htd using (exists_countable_dense <| X ·)

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
⊢ ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)

Tactic:
haveI := fun i ↦ (htc i).to_subtype
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
⊢ Nontrivial ((i : ι) → X i)

Tactic:
nontriviality ∀ i, X i
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabit : ∀ (inhabited_h : Inhabited ((i : ι) → X i)), SeparableSpace ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
inhabit ∀ i, X i
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩

Premises used: Iff.mpr, _private.0.TopologicalSpace.instSeparableSpaceForallOfCountable.match_2, Set.countable_range, Inter.inter, Set.Nonempty, And.intro, Exists.intro, dense_iff_inter_open, Set.range, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
refine :
  ∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
    U.Nonempty → ∀ (g : (i : ι) → X i) (hg : g ∈ U), (U ∩ range f).Nonempty
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
rcases :
  ∀ (I : Finset ι) (u : (a : ι) → Set (X a)) (huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a)
    (huU : (↑I : Set ι).pi (α := X) u ⊆ U), (U ∩ range f).Nonempty
⊢ (U ∩ range f).Nonempty

Tactic:
rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩

Premises used: isOpen_pi_iff, Iff.mp