awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ↦ (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹) (𝓝 x) (𝓝 (infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹)
have refine : (↑x : α) ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α)ᶜ
Tactic: refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
-- 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
⊢ (↑x : α) ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α)ᶜ
have rw : (↑x : α) ∈ (↑s : Set α)
Tactic: rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
-- 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 : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
⊢ t ∈ 𝓝 x
have this : 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 α)ᶜ)⁻¹|))
Tactic: have : Tendsto (fun y : s ↦ dist x.1 y.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist y.1 sᶜ)⁻¹|)
          (𝓝 x) (𝓝 (dist x.1 x.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist x.1 sᶜ)⁻¹|)) := by
        refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs
        refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
        rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
        exact x.2
-- 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 : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹| < ε → y ∈ t
this :
  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 α)ᶜ)⁻¹|))
⊢ t ∈ 𝓝 x
have this₁ : Tendsto (β := ℝ)
  (fun (y : ↥s) ↦ dist (↑x : α) (↑y : α) + |(infDist (↑x : α) (↑s : Set α)ᶜ)⁻¹ - (infDist (↑y : α) (↑s : Set α)ᶜ)⁻¹|)
  (𝓝 x) (𝓝 0)
Tactic: simp only [dist_self, sub_self, abs_zero, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
⊢ CompleteSpace.{u_1} s.CompleteCopy
have refine : ∀ (u : ℕ → s.CompleteCopy) (hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N),
  ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
Tactic: refine Metric.complete_of_convergent_controlled_sequences ((1 / 2) ^ ·) (by simp) fun u hu ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
have refine_1 : ∀ (n m N : ℕ) (hNn : N ≤ n) (hNm : N ≤ m), dist (↑(u n) : α) (↑(u m) : α) ≤ (fun (n : ℕ) ↦ (1 / 2) ^ n) N
Tactic: refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
refine_1 : ∀ (n m N : ℕ) (hNn : N ≤ n) (hNm : N ≤ m), dist (↑(u n) : α) (↑(u m) : α) ≤ (fun (n : ℕ) ↦ (1 / 2) ^ n) N
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
have refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) atTop (𝓝 0)
Tactic: refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
Tactic: have A : CauchySeq fun n => (u n).1 := by
    refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_
    · exact (dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le
    · exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have obtain : ∀ (x : α) (xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
Tactic: obtain ⟨x, xlim⟩ : ∃ x, Tendsto (fun n => (u n).1) atTop (𝓝 x) := cauchySeq_tendsto_of_complete A
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have pos : ∀ (xs : x ∈ s), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
Tactic: by_cases xs : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
pos : ∀ (xs : x ∈ s), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have neg : ∀ (xs : x ∉ s), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
Tactic: by_cases xs : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
⊢ ∃ (C : ℝ), ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
have refine : ∀ (n : ℕ),
  1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0 + 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ
Tactic: refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
n : ℕ
⊢ 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0 + 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ
have rw : 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ - 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0
Tactic: rw [← sub_lt_iff_lt_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have neg : ∀ (C : ℝ) (hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
Tactic: obtain ⟨C, hC⟩ : ∃ C, ∀ n, 1 / infDist (u n).1 sᶜ < C := by
    refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
    rw [← sub_lt_iff_lt_add]
    calc
      _ ≤ |1 / infDist (u n).1 sᶜ - 1 / infDist (u 0).1 sᶜ| := le_abs_self _
      _ = |1 / infDist (u 0).1 sᶜ - 1 / infDist (u n).1 sᶜ| := abs_sub_comm _ _
      _ ≤ dist (u 0) (u n) := le_add_of_nonneg_left dist_nonneg
      _ < (1 / 2) ^ 0 := hu 0 0 n le_rfl n.zero_le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have Cpos : 0 < C
Tactic: have Cpos : 0 < C := lt_of_le_of_lt (div_nonneg zero_le_one infDist_nonneg) (hC 0)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
Cpos : 0 < C
y : α
⊢ y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ
have rw : y ∈ s ↔ y ∉ (↑s : Set α)ᶜ
Tactic: rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
Cpos : 0 < C
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ
Tactic: have Hmem : ∀ {y}, y ∈ s ↔ 0 < infDist y sᶜ := fun {y} ↦ by
    rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]; exact not_not.symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ
n : ℕ
⊢ 1 / C ≤ infDist (↑(u n) : α) (↑s : Set α)ᶜ
have this : 0 < infDist (↑(u n) : α) (↑s : Set α)ᶜ
Tactic: have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ
n : ℕ
this : 0 < infDist (↑(u n) : α) (↑s : Set α)ᶜ
⊢ 1 / C ≤ infDist (↑(u n) : α) (↑s : Set α)ᶜ
have rw : 1 ≤ C * infDist (↑(u n) : α) (↑s : Set α)ᶜ
Tactic: rw [div_le_iff₀' Cpos]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have I : ∀ (n : ℕ), 1 / C ≤ infDist (↑(u n) : α) (↑s : Set α)ᶜ
Tactic: have I : ∀ n, 1 / C ≤ infDist (u n).1 sᶜ := fun n ↦ by
    have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2
    rw [div_le_iff₀' Cpos]
    exact (div_le_iff₀ this).1 (hC n).le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MetricSpace α
s : Opens α
inst_1 : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun (x : ℕ) ↦ (1 / 2) ^ x) N
A : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)
x : α
xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C
Cpos : 0 < C
Hmem : ∀ {y : α}, y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ
I : ∀ (n : ℕ), 1 / C ≤ infDist (↑(u n) : α) (↑s : Set α)ᶜ
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
have I' : 1 / C ≤ infDist x (↑s : Set α)ᶜ
Tactic: have I' : 1 / C ≤ infDist x sᶜ :=
    have : Tendsto (fun n => infDist (u n).1 sᶜ) atTop (𝓝 (infDist x sᶜ)) :=
      ((continuous_infDist_pt (sᶜ : Set α)).tendsto x).comp xlim
    ge_of_tendsto' this I
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsOpen[inst] s
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
⊢ PolishSpace.{u_3} (↑s : Type u_3)
have lift : ∀ (s : Opens α), PolishSpace.{u_3} (↑(↑s : Set α) : Type u_3)
Tactic: lift s to Opens α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
⊢ IsClopenable s
have this : PolishSpace.{u_1} (↑s : Type u_1)
Tactic: haveI : PolishSpace s := hs.polishSpace
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
⊢ IsClopenable s
have this₁ : PolishSpace.{u_1} (↑t : Type u_1)
Tactic: haveI : PolishSpace t := hs.isOpen_compl.polishSpace
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
⊢ coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
have simp : Continuous[instTopologicalSpaceSubtype, inst]
    (comp (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) Sum.inl) ∧
  Continuous[instTopologicalSpaceSubtype, inst]
    (comp (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) Sum.inr)
Tactic: simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
⊢ IsClopenable s
have hle : coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
    instTopologicalSpaceSum ≤
  inst
Tactic: have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
⊢ IsClopenable s
have refine_1 : PolishSpace α
Tactic: refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
refine_1 : PolishSpace α
⊢ IsClopenable s
have refine_2 : IsOpen[coinduced (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) instTopologicalSpaceSum] s
Tactic: refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
this_1 : PolishSpace.{u_1} (↑s : Type u_1)
t : Set α := sᶜ
this : PolishSpace.{u_1} (↑t : Type u_1)
f : (↑s : Type u_1) ⊕ (↑t : Type u_1) ≃ α := Equiv.Set.sumCompl s
hle :
  coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst
⊢ PolishSpace α
have refine_1 : PolishSpace α
Tactic: rw [← f.induced_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
⊢ IsClopenable s
have haveI : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)), IsClopenable s
Tactic: classical
  haveI : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  haveI : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
haveI haveI₁ haveI₂ haveI₃ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)), IsClopenable s
⊢ IsClopenable s
have haveI₄ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
  let t := sᶜ;
  ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)), IsClopenable s
Tactic: classical
  haveI : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  haveI : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Polish (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsClosed[inst] s
haveI haveI₁ haveI₂ haveI₃ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)), IsClopenable s
haveI₄ haveI₅ :
  ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
    let t := sᶜ;
    ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)), IsClopenable s
⊢ IsClopenable s
have haveI₆ : ∀ (this : PolishSpace.{u_1} (↑s : Type u_1)),
  let t := sᶜ;
  ∀ (this : PolishSpace.{u_1} (↑t : Type u_1)),
    let f := Equiv.Set.sumCompl s;
    ∀
      (hle :
        coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
            instTopologicalSpaceSum ≤
          inst),
      IsClopenable s
Tactic: classical
  haveI : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  haveI : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]