awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst : Countable ι
s : ι → Set α
⊢ IsSeparable.{u} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsSeparable (s i)

Tactic:
⟨fun h i ↦ h.mono <| subset_iUnion s i, .iUnion⟩

Premises used: Set.subset_iUnion, TopologicalSpace.IsSeparable.iUnion, Iff.intro, TopologicalSpace.IsSeparable.mono
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
s t : Set α
⊢ IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t

Tactic:
simp [union_eq_iUnion, and_comm]

Premises used: and_comm, Set.union_eq_iUnion
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : IsSeparable u
⊢ IsSeparable (s ∪ u)

Tactic:
isSeparable_union.2 ⟨hs, hu⟩

Premises used: Iff.mpr, TopologicalSpace.isSeparable_union, And.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
⊢ IsSeparable (closure[t] s) ↔ IsSeparable s

Tactic:
simp only [IsSeparable, isClosed_closure.closure_subset_iff]

Premises used: TopologicalSpace.IsSeparable, IsClosed.closure_subset_iff, isClosed_closure
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : s.Countable
⊢ IsSeparable s

Tactic:
⟨s, hs, subset_closure⟩

Premises used: subset_closure, TopologicalSpace.IsSeparable, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s : Set α
hs : s.Finite
⊢ IsSeparable s

Tactic:
hs.countable.isSeparable

Premises used: Set.Countable.isSeparable, Set.Finite.countable
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
inl : ∀ (he : Set.pi (α := X) univ s = ∅), IsSeparable (Set.pi (α := X) univ s)
inr : ∀ (f₀ : (i : ι) → X i), IsSeparable (Set.pi (α := X) univ s)
⊢ IsSeparable (Set.pi (α := X) univ s)

Tactic:
rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩

Premises used: Set.univ, Set.eq_empty_or_nonempty, Set.pi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : Set.pi (α := X) univ s = ∅
inl : IsSeparable (α := (i : ι) → X i) ∅
⊢ IsSeparable (Set.pi (α := X) univ s)

Tactic:
rw [he]
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : Set.pi (α := X) univ s = ∅
⊢ IsSeparable (α := (i : ι) → X i) ∅

Tactic:
countable_empty.isSeparable

Premises used: Set.Countable.isSeparable, Set.countable_empty
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : Set.pi (α := X) univ s = ∅
⊢ IsSeparable (α := (i : ι) → X i) ∅

Tactic:
exact countable_empty.isSeparable

Premises used: Set.Countable.isSeparable, Set.countable_empty
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
f₀ : (i : ι) → X i
inr :
  ∀ (c : (i : ι) → Set (X i)) (c_count : ∀ (i : ι), (c i).Countable) (hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)),
    IsSeparable (Set.pi (α := X) univ s)
⊢ IsSeparable (Set.pi (α := X) univ s)

Tactic:
choose c c_count hc using h
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
⊢ ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)

Tactic:
haveI := fun i ↦ (c_count i).to_subtype
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
⊢ IsSeparable (Set.pi (α := X) univ s)

Tactic:
⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩

Premises used: mem_closure_iff, Iff.mpr, TopologicalSpace.IsSeparable, Set.countable_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
inr :
  ∀ (f : (i : ι) → X i) (hf : f ∈ Set.pi (α := X) univ s) (o : Set ((i : ι) → X i)) (ho : IsOpen[Pi.topologicalSpace] o)
    (hfo : f ∈ o), (o ∩ range g).Nonempty
⊢ IsSeparable (Set.pi (α := X) univ s)

Tactic:
refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
inr :
  ∀ (I : Finset ι) (u : (a : ι) → Set (X a)) (huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a)
    (hI : (↑I : Set ι).pi (α := X) u ⊆ o), (o ∩ range g).Nonempty
⊢ (o ∩ range g).Nonempty

Tactic:
rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩

Premises used: isOpen_pi_iff, Iff.mp
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
inr :
  ∀ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3))
    (hf :
      g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u),
    (o ∩ range g).Nonempty
rsuffices :
  ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
⊢ (o ∩ range g).Nonempty

Tactic:
rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u

Premises used: Set.pi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f_1 : (i : ι) → X i
hf_1 : f_1 ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f_1 ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f_1 a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)
hf : g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
⊢ (o ∩ range g).Nonempty

Tactic:
⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩

Premises used: Set.mem_range_self, Set.Nonempty, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f_1 : (i : ι) → X i
hf_1 : f_1 ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f_1 ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f_1 a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)
hf : g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
⊢ (o ∩ range g).Nonempty

Tactic:
exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
H : ∀ i ∈ I, (u i ∩ c i).Nonempty
choose :
  ∀ (f : (i : ι) → i ∈ I → X i) (hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i) (hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i),
    ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
      g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u

Tactic:
choose f hfu hfc using H
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f_1 : (i : ι) → X i
hf : f_1 ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f_1 ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f_1 a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u

Tactic:
⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩

Premises used: Subtype.mk, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f_1 : (i : ι) → X i
hf : f_1 ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f_1 ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f_1 a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
refine :
  ∀ (i : ι) (hi : i ∈ I),
    g
        (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I fun (i : ↥I) ↦
          Subtype.mk (p := fun (x : X (↑i : ι)) ↦ Membership.mem (γ := Set (X (↑i : ι))) (c (↑i : ι)) x) (f (↑i : ι) ⋯)
            ⋯)
        i ∈
      u i
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u

Tactic:
refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f_1 : (i : ι) → X i
hf : f_1 ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f_1 ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f_1 a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
i : ι
hi : i ∈ I
⊢ g
      (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I fun (i : ↥I) ↦
        Subtype.mk (p := fun (x : X (↑i : ι)) ↦ Membership.mem (γ := Set (X (↑i : ι))) (c (↑i : ι)) x) (f (↑i : ι) ⋯) ⋯)
      i ∈
    u i

Tactic:
simpa only [g, dif_pos hi] using hfu i hi

Premises used: dif_pos
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
suffices : ∀ i ∈ I, (u i ∩ c i).Nonempty
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u

Tactic:
suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
i : ι
hi : i ∈ I
⊢ (u i ∩ c i).Nonempty

Tactic:
mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Premises used: mem_closure_iff, trivial, And.right, And.left, Iff.mp
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
i : ι
hi : i ∈ I
⊢ (u i ∩ c i).Nonempty

Tactic:
exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Premises used: mem_closure_iff, trivial, And.right, And.left, Iff.mp
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
inl : ∀ (he : Set.pi (α := X) univ s = ∅), IsSeparable (Set.pi (α := X) univ s)
inr inr₁ : ∀ (f₀ : (i : ι) → X i), IsSeparable (Set.pi (α := X) univ s)
⊢ IsSeparable (Set.pi (α := X) univ s)

Tactic:
classical
  rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
  · rw [he]
    exact countable_empty.isSeparable
  · choose c c_count hc using h
    haveI := fun i ↦ (c_count i).to_subtype
    set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
    refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
    rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
    rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
    · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
    suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
    intro i hi
    exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Premises used: Set.univ, Set.eq_empty_or_nonempty, Set.Countable.isSeparable, Set.pi, Set.countable_empty
-- Module: Mathlib.Topology.Bases
Goal:
ι : Type u_2
inst : Countable ι
α : ι → Type u_3
s : (i : ι) → Set (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (α := (i : ι) → α i) {f : (i : ι) → α i | ∀ (i : ι), f i ∈ s i}

Tactic:
simpa only [← mem_univ_pi] using IsSeparable.univ_pi h

Premises used: Set.mem_univ_pi, TopologicalSpace.IsSeparable.univ_pi
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
hs : IsSeparable s
ht : IsSeparable t
rcases : ∀ (cs : Set α) (cs_count : cs.Countable) (hcs : s ⊆ closure[t_1] cs), IsSeparable (s ×ˢ t)
⊢ IsSeparable (s ×ˢ t)

Tactic:
rcases hs with ⟨cs, cs_count, hcs⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
ht : IsSeparable t
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t_1] cs
rcases : ∀ (ct : Set β) (ct_count : ct.Countable) (hct : t ⊆ closure[inst] ct), IsSeparable (s ×ˢ t)
⊢ IsSeparable (s ×ˢ t)

Tactic:
rcases ht with ⟨ct, ct_count, hct⟩
-- 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
⊢ IsSeparable (s ×ˢ t)

Tactic:
⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩

Premises used: SProd.sprod, TopologicalSpace.IsSeparable, Set.Countable.prod, And.intro, Exists.intro
-- 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
refine : s ×ˢ t ⊆ closure[instTopologicalSpaceProd] (cs ×ˢ ct)
⊢ IsSeparable (s ×ˢ t)

Tactic:
refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩
-- 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
rw : s ×ˢ t ⊆ closure[t_1] cs ×ˢ closure[inst] ct
⊢ s ×ˢ t ⊆ closure[instTopologicalSpaceProd] (cs ×ˢ ct)

Tactic:
rw [closure_prod_eq]

Premises used: closure_prod_eq