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_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 : ℕ
A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))
⊢ closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (B n)

Tactic:
have I :=
      calc
        closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) :=
          Subset.trans (incl n) inter_subset_left
        _ ⊆ closedEBall (c n) (B n) := closedEBall_subset_closedEBall (rB 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 : ℕ
A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))
I : closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (B n)
⊢ edist (c (n + 1)) (c n) ≤ B n

Tactic:
I A

Premises used: Set.Mem, setOf, Metric.closedEBall
-- 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 : ℕ
A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))
I : closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (B n)
⊢ edist (c (n + 1)) (c n) ≤ B n

Tactic:
exact I A
-- 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 : ℕ), edist (c n) (c (n + 1)) ≤ B n

Tactic:
have cdist : ∀ n, edist (c n) (c (n + 1)) ≤ B n := by
    intro n
    rw [edist_comm]
    have A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1)) := mem_closedEBall_self
    have I :=
      calc
        closedEBall (c (n + 1)) (r (n + 1)) ⊆ closedEBall (c n) (r n) :=
          Subset.trans (incl n) inter_subset_left
        _ ⊆ closedEBall (c n) (B n) := closedEBall_subset_closedEBall (rB n)
    exact I A
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
⊢ CauchySeq c

Tactic:
have : CauchySeq c := cauchySeq_of_edist_le_geometric_two _ ENNReal.one_ne_top cdist
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
rcases :
  ∀ (y : X) (ylim : Tendsto c atTop (nhds y)),
    ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε

Tactic:
rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩

Premises used: cauchySeq_tendsto_of_complete
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
h : Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε

Tactic:
use y
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
h : (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε
⊢ Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε

Tactic:
simp only [Set.mem_iInter]

Premises used: Set.mem_iInter
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
n : ℕ
⊢ ∀ m ≥ n, closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)

Tactic:
Nat.le_induction ?_ fun m _ h => ?_

Premises used: Nat.le_induction
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
n : ℕ
refine_1 : closedEBall (c n) (r n) ⊆ closedEBall (c n) (r n)
refine_2 :
  ∀ (m : ℕ),
    n ≤ m →
      ∀ (h : closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)),
        closedEBall (c (m + 1)) (r (m + 1)) ⊆ closedEBall (c n) (r n)
⊢ ∀ m ≥ n, closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)

Tactic:
refine Nat.le_induction ?_ fun m _ h => ?_
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
n : ℕ
⊢ closedEBall (c n) (r n) ⊆ closedEBall (c n) (r n)

Tactic:
Subset.refl _

Premises used: Set.Subset.refl
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
n : ℕ
⊢ closedEBall (c n) (r n) ⊆ closedEBall (c n) (r n)

Tactic:
exact Subset.refl _

Premises used: Set.Subset.refl
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
n m : ℕ
h_1 : n ≤ m
h : closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)
⊢ closedEBall (c (m + 1)) (r (m + 1)) ⊆ closedEBall (c n) (r n)

Tactic:
Subset.trans (incl m) (Subset.trans inter_subset_left h)

Premises used: Set.Subset.trans, Set.inter_subset_left
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
n m : ℕ
h_1 : n ≤ m
h : closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)
⊢ closedEBall (c (m + 1)) (r (m + 1)) ⊆ closedEBall (c n) (r n)

Tactic:
exact Subset.trans (incl m) (Subset.trans inter_subset_left h)

Premises used: Set.Subset.trans, Set.inter_subset_left
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
⊢ ∀ (n m : ℕ), m ≥ n → closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)

Tactic:
have I : ∀ n, ∀ m ≥ n, closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n) := by
    intro n
    refine Nat.le_induction ?_ fun m _ h => ?_
    · exact Subset.refl _
    · exact Subset.trans (incl m) (Subset.trans inter_subset_left h)
-- 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
cdist : ∀ (n : ℕ), edist (c n) (c (n + 1)) ≤ B n
this : CauchySeq c
y : X
ylim : Tendsto c atTop (nhds y)
I : ∀ (n m : ℕ), m ≥ n → closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)
n : ℕ
⊢ y ∈ closedEBall (c n) (r n)

Tactic:
isClosed_closedEBall.mem_of_tendsto ylim ?_

Premises used: IsClosed.mem_of_tendsto, Metric.isClosed_closedEBall