awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Polish
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) : α)

Tactic:
cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_

Premises used: HDiv.hDiv, cauchySeq_of_le_tendsto_0, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Polish
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
refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) atTop (𝓝 0)
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ (↑(u n) : α)

Tactic:
refine cauchySeq_of_le_tendsto_0 (fun n : ℕ => (1 / 2) ^ n) (fun n m N hNn hNm => ?_) ?_

Premises used: HDiv.hDiv, cauchySeq_of_le_tendsto_0, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Polish
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
n m N : ℕ
hNn : N ≤ n
hNm : N ≤ m
⊢ dist (↑(u n) : α) (↑(u m) : α) ≤ (fun (n : ℕ) ↦ (1 / 2) ^ n) N

Tactic:
(dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le

Premises used: TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Polish
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
n m N : ℕ
hNn : N ≤ n
hNm : N ≤ m
⊢ dist (↑(u n) : α) (↑(u m) : α) ≤ (fun (n : ℕ) ↦ (1 / 2) ^ n) N

Tactic:
exact (dist_val_le_dist (u n) (u m)).trans (hu N n m hNn hNm).le

Premises used: TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Polish
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
⊢ 0 ≤ 1 / 2

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Polish
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
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.Polish
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
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (1 / 2) ^ n) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (by simp) (by norm_num)

Premises used: tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Topology.MetricSpace.Polish
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) : α)

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)
-- Module: Mathlib.Topology.MetricSpace.Polish
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 : α), Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)

Tactic:
cauchySeq_tendsto_of_complete A

Premises used: cauchySeq_tendsto_of_complete
-- Module: Mathlib.Topology.MetricSpace.Polish
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) : α)
obtain :
  ∀ (x : α) (xlim : Tendsto (fun (n : ℕ) ↦ (↑(u n) : α)) atTop (𝓝 x)), ∃ (x : s.CompleteCopy), Tendsto u 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

Premises used: cauchySeq_tendsto_of_complete
-- Module: Mathlib.Topology.MetricSpace.Polish
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)
neg : ∀ (xs : x ∉ s), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)

Tactic:
by_cases xs : x ∈ s
-- Module: Mathlib.Topology.MetricSpace.Polish
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)

Tactic:
⟨⟨x, xs⟩, tendsto_subtype_rng.2 xlim⟩

Premises used: Iff.mpr, Subtype.mk, Exists.intro, tendsto_subtype_rng
-- Module: Mathlib.Topology.MetricSpace.Polish
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)

Tactic:
exact ⟨⟨x, xs⟩, tendsto_subtype_rng.2 xlim⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
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

Tactic:
⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩

Premises used: Compl.compl, Metric.infDist, HDiv.hDiv, SetLike.coe, HPow.hPow, HAdd.hAdd, Exists.intro, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Polish
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
refine :
  ∀ (n : ℕ),
    1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0 + 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ
⊢ ∃ (C : ℝ), ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C

Tactic:
refine ⟨(1 / 2) ^ 0 + 1 / infDist (u 0).1 sᶜ, fun n ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Polish
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 : ℕ
rw : 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ - 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0
⊢ 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0 + 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ

Tactic:
rw [← sub_lt_iff_lt_add]

Premises used: sub_lt_iff_lt_add
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ - 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ ≤
    |1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ - 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ - 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ| =
    |1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ - 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ|

Tactic:
abs_sub_comm _ _

Premises used: abs_sub_comm
-- Module: Mathlib.Topology.MetricSpace.Polish
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 0) : α) (↑s : Set α)ᶜ - 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ| ≤ dist (u 0) (u n)

Tactic:
le_add_of_nonneg_left dist_nonneg

Premises used: dist_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Topology.MetricSpace.Polish
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 : ℕ
⊢ dist (u 0) (u n) < HPow.hPow (β := ℕ) (1 / 2) 0

Tactic:
hu 0 0 n le_rfl n.zero_le

Premises used: Nat.zero_le, le_rfl, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ - 1 / infDist (↑(u 0) : α) (↑s : Set α)ᶜ < HPow.hPow (β := ℕ) (1 / 2) 0

Tactic:
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

Premises used: Nat.zero_le, le_rfl, le_abs_self, Compl.compl, dist_nonneg, Metric.infDist, HDiv.hDiv, SetLike.coe, abs_sub_comm, Dist.dist, OfNat.ofNat, Subtype.val, le_add_of_nonneg_left
-- Module: Mathlib.Topology.MetricSpace.Polish
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
neg :
  ∀ (C : ℝ) (hC : ∀ (n : ℕ), 1 / infDist (↑(u n) : α) (↑s : Set α)ᶜ < C), ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)
⊢ ∃ (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
-- Module: Mathlib.Topology.MetricSpace.Polish
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
⊢ 0 < C

Tactic:
have Cpos : 0 < C := lt_of_le_of_lt (div_nonneg zero_le_one infDist_nonneg) (hC 0)
-- Module: Mathlib.Topology.MetricSpace.Polish
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 : α
rw : y ∈ s ↔ y ∉ (↑s : Set α)ᶜ
⊢ y ∈ s ↔ 0 < infDist y (↑s : Set α)ᶜ

Tactic:
rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]

Premises used: IsOpen.isClosed_compl, TopologicalSpace.Opens.isOpen, Exists.intro, IsClosed.notMem_iff_infDist_pos
-- Module: Mathlib.Topology.MetricSpace.Polish
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 ↔ y ∉ (↑s : Set α)ᶜ

Tactic:
not_not.symm

Premises used: Classical.not_not, Set.Mem, setOf, Not, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Polish
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 ↔ y ∉ (↑s : Set α)ᶜ

Tactic:
exact not_not.symm

Premises used: Classical.not_not, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ

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
-- Module: Mathlib.Topology.MetricSpace.Polish
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 : ℕ
⊢ 0 < infDist (↑(u n) : α) (↑s : Set α)ᶜ

Tactic:
have : 0 < infDist (u n).1 sᶜ := Hmem.1 (u n).2
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ
rw : 1 ≤ C * infDist (↑(u n) : α) (↑s : Set α)ᶜ
⊢ 1 / C ≤ infDist (↑(u n) : α) (↑s : Set α)ᶜ

Tactic:
rw [div_le_iff₀' Cpos]

Premises used: div_le_iff₀'
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ

Tactic:
(div_le_iff₀ this).1 (hC n).le

Premises used: div_le_iff₀, LT.lt.le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ

Tactic:
exact (div_le_iff₀ this).1 (hC n).le

Premises used: div_le_iff₀, LT.lt.le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ

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
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ
⊢ 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
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ
I' : 1 / C ≤ infDist x (↑s : Set α)ᶜ
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)

Tactic:
absurd (Hmem.2 <| lt_of_lt_of_le (div_pos one_pos Cpos) I') xs

Premises used: Iff.mpr, absurd, div_pos, one_pos, lt_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Polish
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 α)ᶜ
I' : 1 / C ≤ infDist x (↑s : Set α)ᶜ
⊢ ∃ (x : s.CompleteCopy), Tendsto u atTop (𝓝 x)

Tactic:
exact absurd (Hmem.2 <| lt_of_lt_of_le (div_pos one_pos Cpos) I') xs

Premises used: Iff.mpr, absurd, div_pos, one_pos, lt_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsOpen[inst] s
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
⊢ IsOpen[inst] s

Tactic:
hs
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : PolishSpace α
s : Set α
hs : IsOpen[inst] s
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
lift : ∀ (s : Opens α), PolishSpace.{u_3} (↑(↑s : Set α) : Type u_3)
⊢ PolishSpace.{u_3} (↑s : Type u_3)

Tactic:
lift s to Opens α using hs

Premises used: TopologicalSpace.Opens
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : PolishSpace α
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
s : Opens α
⊢ PolishSpace.{u_3} (↑(↑s : Set α) : Type u_3)

Tactic:
inferInstanceAs (PolishSpace s.CompleteCopy)

Premises used: _private.0.IsOpen.polishSpace._proof_1
-- Module: Mathlib.Topology.MetricSpace.Polish
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : PolishSpace α
this : UpgradedIsCompletelyMetrizableSpace α := upgradeIsCompletelyMetrizable α
s : Opens α
⊢ PolishSpace.{u_3} (↑(↑s : Set α) : Type u_3)

Tactic:
exact inferInstanceAs (PolishSpace s.CompleteCopy)
-- 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:
haveI : PolishSpace s := hs.polishSpace
-- Module: Mathlib.Topology.MetricSpace.Polish
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ᶜ
⊢ PolishSpace.{u_1} (↑t : Type u_1)

Tactic:
haveI : PolishSpace t := hs.isOpen_compl.polishSpace
-- Module: Mathlib.Topology.MetricSpace.Polish
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
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)
⊢ coinduced (X := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (⇑f : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
      instTopologicalSpaceSum ≤
    inst

Tactic:
simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]

Premises used: instTopologicalSpaceSum, sup_le_iff, coinduced_compose, coinduced_sup, continuous_iff_coinduced_le