awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
⊢ ∀ (n : ℕ) (x_1 : X) (δ : ℝ≥0∞),
    δ ≠ 0 → ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x_1 δ ∩ f n

Tactic:
have : ∀ n x δ, δ ≠ 0 →
      ∃ y r, 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n := by
    intro n x δ δpos
    have : x ∈ closure (f n) := hd n x
    rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
    rw [edist_comm] at xy
    obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedEBall y r ⊆ f n :=
      nhds_basis_closedEBall.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)
    refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
    · show 0 < min (min (δ / 2) r) (B (n + 1))
      exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))
    · show min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
      exact min_le_right _ _
    · show z ∈ closedEBall x δ
      calc
        edist z x ≤ edist z y + edist y x := edist_triangle _ _ _
        _ ≤ min (min (δ / 2) r) (B (n + 1)) + δ / 2 := add_le_add hz (le_of_lt xy)
        _ ≤ δ / 2 + δ / 2 := (add_le_add (le_trans (min_le_left _ _) (min_le_left _ _)) le_rfl)
        _ = δ := ENNReal.add_halves δ
    show z ∈ f n
    exact hr (calc
      edist z y ≤ min (min (δ / 2) r) (B (n + 1)) := hz
      _ ≤ r := le_trans (min_le_left _ _) (min_le_right _ _))
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
this :
  ∀ (n : ℕ) (x_1 : X) (δ : ℝ≥0∞),
    δ ≠ 0 → ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x_1 δ ∩ f n
choose! :
  ∀ (center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X) (radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞)
    (Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ)
    (HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1))
    (Hball :
      ∀ (n : ℕ) (x_1 : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x_1 δ) (radius n x_1 δ) ⊆ closedEBall x_1 δ ∩ f n),
    Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
choose! center radius Hpos HB Hball using this

Premises used: Set.center
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x_1 : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x_1 δ) (radius n x_1 δ) ⊆ closedEBall x_1 δ ∩ f n
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
fun x => (mem_closure_iff_nhds_basis nhds_basis_closedEBall).2 fun ε εpos => ?_

Premises used: Iff.mpr, Set.Mem, Dense, Metric.nhds_basis_closedEBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x_1 : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x_1 δ) (radius n x_1 δ) ⊆ closedEBall x_1 δ ∩ f n
refine :
  ∀ (x_1 : X) (ε : ℝ≥0∞) (εpos : 0 < ε),
    ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x_1 ε
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
refine fun x => (mem_closure_iff_nhds_basis nhds_basis_closedEBall).2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedEBall, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
⊢ 0 < r 0

Tactic:
lt_min εpos (Bpos 0)

Premises used: lt_min, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
⊢ 0 < r 0

Tactic:
exact lt_min εpos (Bpos 0)

Premises used: lt_min, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
n : ℕ
hn : 0 < r n
⊢ 0 < r (n + 1)

Tactic:
Hpos n (c n) (r n) hn.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
n : ℕ
hn : 0 < r n
⊢ 0 < r (n + 1)

Tactic:
exact Hpos n (c n) (r n) hn.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
n : ℕ
zero : 0 < r 0
succ : ∀ (n : ℕ) (hn : 0 < r n), 0 < r (n + 1)
⊢ 0 < r n

Tactic:
induction n with
    | zero => exact lt_min εpos (Bpos 0)
    | succ n hn => exact Hpos n (c n) (r n) hn.ne'

Premises used: lt_min, OfNat.ofNat
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
⊢ ∀ (n : ℕ), 0 < r n

Tactic:
have rpos : ∀ n, 0 < r n := by
    intro n
    induction n with
    | zero => exact lt_min εpos (Bpos 0)
    | succ n hn => exact Hpos n (c n) (r n) hn.ne'
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
⊢ ∀ (n : ℕ), r n ≠ 0

Tactic:
have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
⊢ r 0 ≤ B 0

Tactic:
min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
⊢ r 0 ≤ B 0

Tactic:
exact min_le_right _ _

Premises used: min_le_right
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
⊢ r (n + 1) ≤ B (n + 1)

Tactic:
HB n (c n) (r n) (r0 n)
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
⊢ r (n + 1) ≤ B (n + 1)

Tactic:
exact HB n (c n) (r n) (r0 n)
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
n : ℕ
zero : r 0 ≤ B 0
succ : ∀ (n : ℕ), r (n + 1) ≤ B (n + 1)
⊢ r n ≤ B n

Tactic:
cases n with
    | zero => exact min_le_right _ _
    | succ n => exact HB n (c n) (r n) (r0 n)

Premises used: min_le_right
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
⊢ ∀ (n : ℕ), r n ≤ B n

Tactic:
have rB : ∀ n, r n ≤ B n := by
    intro n
    cases n with
    | zero => exact min_le_right _ _
    | succ n => exact HB n (c n) (r n) (r0 n)
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
⊢ ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n

Tactic:
have incl : ∀ n, closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n :=
    fun n => Hball n (c n) (r n) (r0 n)
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
n : ℕ
rw : edist (c (n + 1)) (c n) ≤ B n
⊢ edist (c n) (c (n + 1)) ≤ B n

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.Baire.CompleteMetrizable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
center : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → X
radius : (n : ℕ) → (x : X) → (δ : ℝ≥0∞) → ℝ≥0∞
Hpos : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → 0 < radius n x δ
HB : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → radius n x δ ≤ B (n + 1)
Hball : ∀ (n : ℕ) (x : X) (δ : ℝ≥0∞), δ ≠ 0 → closedEBall (center n x δ) (radius n x δ) ⊆ closedEBall x δ ∩ f n
x : X
ε : ℝ≥0∞
εpos : 0 < ε
F : ℕ → X × ℝ≥0∞ :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ X × ℝ≥0∞) n (x, min ε (B 0)) fun (n : ℕ) (p : X × ℝ≥0∞) ↦
      (center n p.1 p.2, radius n p.1 p.2)
c : ℕ → X := fun (n : ℕ) ↦ (F n).1
r : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ (F n).2
rpos : ∀ (n : ℕ), 0 < r n
r0 : ∀ (n : ℕ), r n ≠ 0
rB : ∀ (n : ℕ), r n ≤ B n
incl : ∀ (n : ℕ), closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) ∩ f n
n : ℕ
⊢ c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))

Tactic:
have A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1)) := mem_closedEBall_self