awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : X) ↦ denseSeq X n

Tactic:
continuous_const (y := denseSeq X n)

Premises used: continuous_const
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : X) ↦ denseSeq X n

Tactic:
convert! continuous_const (y := denseSeq X n)

Premises used: continuous_const
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
inl :
  ∀ (hC : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ = ∅),
    ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
inr :
  ∀ (hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty),
    ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
obtain hC | hC := (closure Cᶜ).eq_empty_or_nonempty

Premises used: Compl.compl, Set.eq_empty_or_nonempty, closure
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ = ∅
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
simp_all
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
⊢ Nonempty X

Tactic:
have : Nonempty X := ⟨x⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
⊢ ε / 2 > 0

Tactic:
simp_all [ε, ← IsClosed.notMem_iff_infDist_pos, mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds, IsClosed.notMem_iff_infDist_pos
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
inr : ∀ (n : ℕ) (hn : dist x (denseSeq X n) < ε / 2), ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
obtain ⟨n, hn⟩ := denseRange_iff.mp (denseRange_denseSeq X) x (ε / 2)
    (by simp_all [ε, ← IsClosed.notMem_iff_infDist_pos, mem_interior_iff_mem_nhds])

Premises used: TopologicalSpace.denseRange_denseSeq, HDiv.hDiv, Iff.mp, Metric.denseRange_iff, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
⟨n, ball 0 (ε / 2), isOpen_ball.mem_nhds ?_, ?_⟩

Premises used: HDiv.hDiv, Metric.ball, Metric.isOpen_ball, And.intro, IsOpen.mem_nhds, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
inr : Membership.mem (γ := Set (↑I : Type)) (ball 0 (ε / 2)) (distDenseSeq X n x)
inr₁ : distDenseSeq X n ⁻¹' ball 0 (ε / 2) ⊆ C
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
refine ⟨n, ball 0 (ε / 2), isOpen_ball.mem_nhds ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
⊢ Membership.mem (γ := Set (↑I : Type)) (ball 0 (ε / 2)) (distDenseSeq X n x)

Tactic:
simp [Subtype.dist_eq, abs_eq_self.mpr, coe_projIcc, hn]

Premises used: Iff.mpr, Set.coe_projIcc, Subtype.dist_eq, abs_eq_self
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : y ∈ distDenseSeq X n ⁻¹' ball 0 (ε / 2)
⊢ dist y (denseSeq X n) < ε / 2

Tactic:
simpa [Subtype.dist_eq, abs_eq_self.mpr, coe_projIcc, not_lt_of_ge, ε, div_le_iff₀] using hy

Premises used: Iff.mpr, div_le_iff₀, Set.coe_projIcc, Subtype.dist_eq, abs_eq_self, not_lt_of_ge
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : y ∈ distDenseSeq X n ⁻¹' ball 0 (ε / 2)
⊢ dist y (denseSeq X n) < ε / 2

Tactic:
replace hy : dist y (denseSeq X n) < ε / 2 := by
      simpa [Subtype.dist_eq, abs_eq_self.mpr, coe_projIcc, not_lt_of_ge, ε, div_le_iff₀] using hy
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : dist y (denseSeq X n) < ε / 2
⊢ ε / 2 + ε / 2 ≤ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)

Tactic:
simp [ε]
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : dist y (denseSeq X n) < ε / 2
⊢ dist x y < infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)

Tactic:
have : dist x y < infDist x (closure Cᶜ) :=
      ((dist_triangle_right x y (denseSeq X n)).trans_lt (add_lt_add hn hy)).trans_le (by simp [ε])
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this_1 : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : dist y (denseSeq X n) < ε / 2
this : dist x y < infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)
⊢ y ∈ C

Tactic:
simpa using notMem_of_notMem_closure (mt infDist_le_dist_of_mem this.not_ge)

Premises used: Metric.infDist_le_dist_of_mem, mt, notMem_of_notMem_closure, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x y : X
hxy : x ≠ y
obtain :
  ∀ (n : ℕ) (hn : {y}ᶜ ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))),
    ∃ (n : ℕ), distDenseSeq X n x ≠ distDenseSeq X n y
⊢ ∃ (n : ℕ), distDenseSeq X n x ≠ distDenseSeq X n y

Tactic:
obtain ⟨n, hn⟩ := separation ((isOpen_compl_singleton (x := y)).mem_nhds hxy)

Premises used: Metric.PiNatEmbed.separation, isOpen_compl_singleton, IsOpen.mem_nhds
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x y : X
hxy : x ≠ y
n : ℕ
hn : {y}ᶜ ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
e : distDenseSeq X n x = distDenseSeq X n y
⊢ False

Tactic:
simp +contextual [e, ← exists_prop, mem_of_mem_nhds] at hn

Premises used: mem_of_mem_nhds, exists_prop
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x y : X
hxy : x ≠ y
n : ℕ
hn : {y}ᶜ ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
⊢ ∃ (n : ℕ), distDenseSeq X n x ≠ distDenseSeq X n y

Tactic:
exact ⟨n, fun e ↦ by simp +contextual [e, ← exists_prop, mem_of_mem_nhds] at hn⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))

Tactic:
continuous_iff_continuousAt.mpr fun x s hs ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
refine :
  ∀ (x : PiNatEmbed X (fun (x : ℕ) ↦ (↑I : Type)) (distDenseSeq X)) (s : Set X)
    (hs : s ∈ 𝓝 (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))), s ∈ map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))) (𝓝 x)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))

Tactic:
refine continuous_iff_continuousAt.mpr fun x s hs ↦ ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : PiNatEmbed X (fun (x : ℕ) ↦ (↑I : Type)) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
obtain :
  ∀ (i : ℕ) (t : Set (↑I : Type)) (ht : t ∈ 𝓝 (distDenseSeq X i (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))))
    (hts : distDenseSeq X i ⁻¹' t ⊆ s), s ∈ map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))) (𝓝 x)
⊢ s ∈ map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))) (𝓝 x)

Tactic:
obtain ⟨i, t, ht, hts⟩ := separation hs

Premises used: Metric.PiNatEmbed.separation
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : PiNatEmbed X (fun (x : ℕ) ↦ (↑I : Type)) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
i : ℕ
t : Set (↑I : Type)
ht : t ∈ 𝓝 (distDenseSeq X i (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))))
hts : distDenseSeq X i ⁻¹' t ⊆ s
rw :
  s ∈
    map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
      (comap (embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X))
        (Filter.pi (α := fun (i : ℕ) ↦ (↑I : Type)) fun (i : ℕ) ↦
          𝓝 (embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) x i)))
⊢ s ∈ map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))) (𝓝 x)

Tactic:
rw [(isUniformEmbedding_embed injective_distDenseSeq).isEmbedding.nhds_eq_comap, nhds_pi]

Premises used: Topology.IsInducing.nhds_eq_comap, nhds_pi, Metric.PiNatEmbed.injective_distDenseSeq, Topology.IsEmbedding.toIsInducing, IsUniformEmbedding.isEmbedding, Metric.PiNatEmbed.isUniformEmbedding_embed
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : PiNatEmbed X (fun (x : ℕ) ↦ (↑I : Type)) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
i : ℕ
t : Set (↑I : Type)
ht : t ∈ 𝓝 (distDenseSeq X i (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))))
hts : distDenseSeq X i ⁻¹' t ⊆ s
⊢ s ∈
    map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
      (comap (embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X))
        (Filter.pi (α := fun (i : ℕ) ↦ (↑I : Type)) fun (i : ℕ) ↦
          𝓝 (embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) x i)))

Tactic:
⟨_, Filter.mem_pi_of_mem _ ht, fun x hx ↦ hts hx⟩

Premises used: Set.Mem, setOf, Filter.mem_pi_of_mem, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x : PiNatEmbed X (fun (x : ℕ) ↦ (↑I : Type)) (distDenseSeq X)
s : Set X
hs : s ∈ 𝓝 (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
i : ℕ
t : Set (↑I : Type)
ht : t ∈ 𝓝 (distDenseSeq X i (x.ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))))
hts : distDenseSeq X i ⁻¹' t ⊆ s
⊢ s ∈
    map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
      (comap (embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X))
        (Filter.pi (α := fun (i : ℕ) ↦ (↑I : Type)) fun (i : ℕ) ↦
          𝓝 (embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) x i)))

Tactic:
exact ⟨_, Filter.mem_pi_of_mem _ ht, fun x hx ↦ hts hx⟩
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
firststep : X ≃ₜ PiNatEmbed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) :=
  { toFun := toPiNat (Y := fun (i : ℕ) ↦ (↑I : Type)), invFun := ofPiNat (Y := fun (i : ℕ) ↦ (↑I : Type)),
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
secondstep : PiNatEmbed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) → ℕ → (↑I : Type) :=
  embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X)
isEmbedding_secondstep : IsEmbedding secondstep := ⋯
⊢ ∃ (F : X → ℕ → (↑I : Type)), IsEmbedding F

Tactic:
⟨_, isEmbedding_secondstep.comp firststep.isEmbedding⟩

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PiNat
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
firststep : X ≃ₜ PiNatEmbed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) :=
  { toFun := toPiNat (Y := fun (i : ℕ) ↦ (↑I : Type)), invFun := ofPiNat (Y := fun (i : ℕ) ↦ (↑I : Type)),
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
secondstep : PiNatEmbed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X) → ℕ → (↑I : Type) :=
  embed X (fun (i : ℕ) ↦ (↑I : Type)) (distDenseSeq X)
isEmbedding_secondstep : IsEmbedding secondstep := ⋯
⊢ ∃ (F : X → ℕ → (↑I : Type)), IsEmbedding F

Tactic:
exact ⟨_, isEmbedding_secondstep.comp firststep.isEmbedding⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeparableSpace α
inst_2 : IsCompletelyMetrizableSpace α
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
⊢ SecondCountableTopology α

Tactic:
haveI := UniformSpace.secondCountable_of_separable α
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeparableSpace α
inst_2 : IsCompletelyMetrizableSpace α
this_1 : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
this : SecondCountableTopology α
⊢ PolishSpace α

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : PolishSpace α
inst_2 : Nonempty α
⊢ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ Surjective f

Tactic:
letI := upgradeIsCompletelyMetrizable α
  exists_nat_nat_continuous_surjective_of_completeSpace α

Premises used: exists_nat_nat_continuous_surjective_of_completeSpace
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
⊢ SecondCountableTopology α

Tactic:
haveI : SecondCountableTopology α := hf.isEmbedding.secondCountableTopology
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this_2 : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
rw : IsComplete (range f)
⊢ CompleteSpace α

Tactic:
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.to_isometry, Isometry.isUniformInducing, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this_2 : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ IsComplete (range f)

Tactic:
hf.isClosed_range.isComplete

Premises used: IsClosed.isComplete, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this_2 : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ IsComplete (range f)

Tactic:
exact hf.isClosed_range.isComplete

Premises used: IsClosed.isComplete, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this_2 : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ CompleteSpace α

Tactic:
have : CompleteSpace α := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this_1 : UpgradedIsCompletelyMetrizableSpace β := upgradeIsCompletelyMetrizable β
this_2 : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this_3 : SecondCountableTopology α
this : CompleteSpace α
⊢ PolishSpace α

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : PolishSpace β
f : α ≃ β
⊢ PolishSpace α

Tactic:
letI : TopologicalSpace α := t.induced f
  (f.toHomeomorphOfIsInducing ⟨rfl⟩).isClosedEmbedding.polishSpace

Premises used: Topology.IsClosedEmbedding.polishSpace, Topology.IsInducing.mk, Equiv.toHomeomorphOfIsInducing, Homeomorph.isClosedEmbedding, rfl
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
⊢ PolishSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isClosedEmbedding_subtypeVal.polishSpace

Premises used: Topology.IsClosedEmbedding.polishSpace, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ (t₀ : TopologicalSpace α), T2Space α ∧ ∀ (i : ι), t i ≤ t₀
ht :
  ∀ (i : ι),
    ∃ (u : UniformSpace α), CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ UniformSpace.toTopologicalSpace = t i
choose :
  ∀ (u : (i : ι) → UniformSpace α) (hcomp : ∀ (i : ι), CompleteSpace α) (hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated)
    (hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = t i),
    ∃ (u : UniformSpace α),
      CompleteSpace α ∧
        (𝓤 α).IsCountablyGenerated ∧
          Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
⊢ ∃ (u : UniformSpace α),
    CompleteSpace α ∧
      (𝓤 α).IsCountablyGenerated ∧
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)

Tactic:
choose u hcomp hcount hut using ht
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ (t₀ : TopologicalSpace α), T2Space α ∧ ∀ (i : ι), t i ≤ t₀
u : (i : ι) → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = t i
⊢ t = fun (i : ι) ↦ UniformSpace.toTopologicalSpace

Tactic:
(funext hut).symm

Premises used: funext, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ (t₀ : TopologicalSpace α), T2Space α ∧ ∀ (i : ι), t i ≤ t₀
u : (i : ι) → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = t i
obtain :
  ∀
    (ht₀ :
      ∃ (t₀ : TopologicalSpace α),
        T2Space α ∧ ∀ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i ≤ t₀)
    (hut :
      ∀ (i : ι),
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
          ((fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)),
    ∃ (u_1 : UniformSpace α),
      CompleteSpace α ∧
        (𝓤 α).IsCountablyGenerated ∧
          Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
            (⨅ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)
⊢ ∃ (u : UniformSpace α),
    CompleteSpace α ∧
      (𝓤 α).IsCountablyGenerated ∧
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)

Tactic:
obtain rfl : t = fun i ↦ (u i).toTopologicalSpace := (funext hut).symm

Premises used: funext, Eq.symm, UniformSpace.toTopologicalSpace, rfl
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
u : (i : ι) → UniformSpace α
hcomp : ∀ (i : ι), CompleteSpace α
hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated
ht₀ :
  ∃ (t₀ : TopologicalSpace α),
    T2Space α ∧ ∀ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i ≤ t₀
hut :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
      ((fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)
⊢ ∃ (u_1 : UniformSpace α),
    CompleteSpace α ∧
      (𝓤 α).IsCountablyGenerated ∧
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace
          (⨅ (i : ι), (fun (i : ι) ↦ (UniformSpace.toTopologicalSpace : TopologicalSpace α)) i)

Tactic:
⟨⨅ i, u i, .iInf hcomp ht₀, ?_, UniformSpace.toTopologicalSpace_iInf⟩

Premises used: iInf, UniformSpace.toTopologicalSpace_iInf, CompleteSpace.iInf, And.intro, Exists.intro