awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst : Encodable ι
inst_1 : (i : ι) → MetricSpace (Y i)
inst_2 : TopologicalSpace X
inst_3 : CompactSpace X
continuous_f : ∀ (i : ι), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
separating_f : Pairwise fun (x y : X) ↦ ∃ (i : ι), f i x ≠ f i y
this : EMetricSpace (PiNatEmbed X Y f) := emetricSpace (Y := Y) separating_f
⊢ IsHomeomorph.{u_3, u_3} (X := X) (Y := PiNatEmbed X Y f) (toPiNat (Y := Y))
have rw : Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (toPiNat (Y := Y)) ∧
  Bijective.{u_3 + 1, u_3 + 1} (α := X) (β := PiNatEmbed X Y f) (toPiNat (Y := Y))
Tactic: rw [isHomeomorph_iff_continuous_bijective]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
have inl : IsEmpty X → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
inl : IsEmpty X → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
have inr : Nonempty X → Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
n : ℕ
h : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
have inr : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  fun (x : X) ↦ denseSeq X n
Tactic: refine continuous_projIcc.comp <| Continuous.dist continuous_id' ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
have inl : ∀ (hC : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ = ∅),
  ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
Tactic: obtain hC | hC := (closure Cᶜ).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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))
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
have inr : ∀ (hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty),
  ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
Tactic: obtain hC | hC := (closure Cᶜ).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
have this : Nonempty X
Tactic: have : Nonempty X := ⟨x⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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 : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
have inr : ∀ (n : ℕ) (hn : dist x (denseSeq X n) < ε / 2), ∃ (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])
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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))
have inr : Membership.mem (γ := Set (↑I : Type)) (ball 0 (ε / 2)) (distDenseSeq X n x)
Tactic: refine ⟨n, ball 0 (ε / 2), isOpen_ball.mem_nhds ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)
⊢ ∃ (n : ℕ), C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))
have inr₁ : distDenseSeq X n ⁻¹' ball 0 (ε / 2) ⊆ C
Tactic: refine ⟨n, ball 0 (ε / 2), isOpen_ball.mem_nhds ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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)
⊢ y ∈ C
have hy₁ : 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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (hypothesis)
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
⊢ y ∈ C
have this₁ : 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 [ε])
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
x y : X
hxy : x ≠ y
⊢ ∃ (n : ℕ), distDenseSeq X n x ≠ distDenseSeq X n y
have obtain : ∀ (n : ℕ) (hn : {y}ᶜ ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))),
  ∃ (n : ℕ), distDenseSeq X n x ≠ distDenseSeq X n y
Tactic: obtain ⟨n, hn⟩ := separation ((isOpen_compl_singleton (x := y)).mem_nhds hxy)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
Goal:
X : Type u_3
inst : MetricSpace X
inst_1 : SeparableSpace X
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type)))
have 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)
Tactic: refine continuous_iff_continuousAt.mpr fun x s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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)))
⊢ s ∈ map (ofPiNat (Y := fun (x : ℕ) ↦ (↑I : Type))) (𝓝 x)
have 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)
Tactic: obtain ⟨i, t, ht, hts⟩ := separation hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PiNat (goal)
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))) (𝓝 x)
have 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)))
Tactic: rw [(isUniformEmbedding_embed injective_distDenseSeq).isEmbedding.nhds_eq_comap, nhds_pi]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeparableSpace α
inst_2 : IsCompletelyMetrizableSpace α
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
⊢ PolishSpace α
have this₁ : SecondCountableTopology α
Tactic: haveI := UniformSpace.secondCountable_of_separable α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
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 ⋯
⊢ PolishSpace α
have this₁ : SecondCountableTopology α
Tactic: haveI : SecondCountableTopology α := hf.isEmbedding.secondCountableTopology
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
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 α
have rw : IsComplete (range f)
Tactic: rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
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 α
⊢ PolishSpace α
have this₁ : CompleteSpace α
Tactic: have : CompleteSpace α := by
    rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
    exact hf.isClosed_range.isComplete
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
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
⊢ ∃ (u : UniformSpace α),
    CompleteSpace α ∧
      (𝓤 α).IsCountablyGenerated ∧
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
have 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)
Tactic: choose u hcomp hcount hut using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
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
⊢ ∃ (u : UniformSpace α),
    CompleteSpace α ∧
      (𝓤 α).IsCountablyGenerated ∧
        Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
have 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)
Tactic: obtain rfl : t = fun i ↦ (u i).toTopologicalSpace := (funext hut).symm
Cleared hypotheses: t, ht₀, hut
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
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)
have refine : (𝓤 α).IsCountablyGenerated
Tactic: refine ⟨⨅ i, u i, .iInf hcomp ht₀, ?_, UniformSpace.toTopologicalSpace_iInf⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
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)
⊢ (𝓤 α).IsCountablyGenerated
have rw : IsCountablyGenerated.{u_1} (α := α × α) (⨅ (i : ι), 𝓤 α)
Tactic: rw [iInf_uniformity]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ (i₀ : ι), ∀ (i : ι), t i ≤ t i₀
ht : ∀ (i : ι), PolishSpace α
⊢ PolishSpace α
have rcases : ∀ (i₀ : ι) (hi₀ : ∀ (i : ι), t i ≤ t i₀), PolishSpace α
Tactic: rcases ht₀ with ⟨i₀, hi₀⟩
Cleared hypotheses: ht₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
⊢ PolishSpace α
have rcases : ∀ (u : UniformSpace α) (hcomp : CompleteSpace α) (hcount : (𝓤 α).IsCountablyGenerated)
  (htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)), PolishSpace α
Tactic: rcases CompletePseudometrizable.iInf ⟨t i₀, letI := t i₀; haveI := ht i₀; inferInstance, hi₀⟩
    fun i ↦
      letI := t i; haveI := ht i; letI := upgradeIsCompletelyMetrizable α
      ⟨inferInstance, inferInstance, inferInstance, rfl⟩
    with ⟨u, hcomp, hcount, htop⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
⊢ PolishSpace α
have rw : PolishSpace α
Tactic: rw [← htop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
⊢ PolishSpace α
have this : SecondCountableTopology α
Tactic: have : @SecondCountableTopology α u.toTopologicalSpace :=
    htop.symm ▸ secondCountableTopology_iInf fun i ↦ letI := t i; (ht i).toSecondCountableTopology
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
this_1 : SecondCountableTopology α
this : TopologicalSpace α := t i₀
⊢ T1Space α
have this₁ : PolishSpace α
Tactic: haveI := ht i₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), PolishSpace α
i₀ : ι
hi₀ : ∀ (i : ι), t i ≤ t i₀
u : UniformSpace α
hcomp : CompleteSpace α
hcount : (𝓤 α).IsCountablyGenerated
htop : Eq.{u_1 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace (⨅ (i : ι), t i)
this : SecondCountableTopology α
⊢ PolishSpace α
have this₁ : T1Space α
Tactic: have : @T1Space α u.toTopologicalSpace :=
    htop.symm ▸ t1Space_antitone (iInf_le _ i₀) (by letI := t i₀; haveI := ht i₀; infer_instance)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
⊢ MetricSpace s.CompleteCopy
have refine_1 : ∀ (x : s.CompleteCopy), dist x x = 0
Tactic: refine @MetricSpace.ofT0PseudoMetricSpace (CompleteCopy s)
    (.ofDistTopology dist (fun _ ↦ ?_) (fun _ _ ↦ ?_) (fun x y z ↦ ?_) fun t ↦ ?_) _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
refine_1 : ∀ (x : s.CompleteCopy), dist x x = 0
⊢ MetricSpace s.CompleteCopy
have refine_2 : ∀ (x x_1 : s.CompleteCopy), dist x x_1 = dist x_1 x
Tactic: refine @MetricSpace.ofT0PseudoMetricSpace (CompleteCopy s)
    (.ofDistTopology dist (fun _ ↦ ?_) (fun _ _ ↦ ?_) (fun x y z ↦ ?_) fun t ↦ ?_) _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
refine_1 : ∀ (x : s.CompleteCopy), dist x x = 0
refine_2 : ∀ (x x_1 : s.CompleteCopy), dist x x_1 = dist x_1 x
⊢ MetricSpace s.CompleteCopy
have refine_3 : ∀ (x y z : s.CompleteCopy), dist x z ≤ dist x y + dist y z
Tactic: refine @MetricSpace.ofT0PseudoMetricSpace (CompleteCopy s)
    (.ofDistTopology dist (fun _ ↦ ?_) (fun _ _ ↦ ?_) (fun x y z ↦ ?_) fun t ↦ ?_) _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
refine_1 : ∀ (x : s.CompleteCopy), dist x x = 0
refine_2 : ∀ (x x_1 : s.CompleteCopy), dist x x_1 = dist x_1 x
refine_3 : ∀ (x y z : s.CompleteCopy), dist x z ≤ dist x y + dist y z
⊢ MetricSpace s.CompleteCopy
have refine_4 : ∀ (t : Set s.CompleteCopy), IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
Tactic: refine @MetricSpace.ofT0PseudoMetricSpace (CompleteCopy s)
    (.ofDistTopology dist (fun _ ↦ ?_) (fun _ _ ↦ ?_) (fun x y z ↦ ?_) fun t ↦ ?_) _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
have refine_4 : ∀ (h : IsOpen t) (x : s.CompleteCopy) (hx : x ∈ t), ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
refine_4 : ∀ (h : IsOpen t) (x : s.CompleteCopy) (hx : x ∈ t), ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
have refine_4₁ : ∀ (h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t) (x : s.CompleteCopy) (hx : x ∈ t), t ∈ 𝓝 x
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : IsOpen t
x : s.CompleteCopy
hx : x ∈ t
⊢ ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
have refine_4 : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball x ε ⊆ t), ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
Tactic: rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
⊢ t ∈ 𝓝 x
have refine_4 : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t), t ∈ 𝓝 x
Tactic: rcases h x hx with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε : ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
⊢ t ∈ 𝓝 x
have hε₁ : ∀ (y : s.CompleteCopy),
  dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
Tactic: simp only [dist_eq, one_div] at hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
h : ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t
x : s.CompleteCopy
hx : x ∈ t
ε : ℝ
ε0 : ε > 0
hε :
  ∀ (y : s.CompleteCopy),
    dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ Tendsto
    (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
    (𝓝 x) (𝓝 (dist (↑x : α) (↑x : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹|))
have refine : Tendsto (fun (y : ↥s) ↦ (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹) (𝓝 x) (𝓝 (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹)
Tactic: refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs