Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : 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 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → 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 n (x, min ε (B 0)) fun n p ↦ (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:
refine Nat.le_induction ?_ fun m _ h => ?_

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : 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 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → 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 n (x, min ε (B 0)) fun n p ↦ (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)

case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : 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 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
center : ℕ → X → ℝ≥0∞ → X
radius : ℕ → 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 n (x, min ε (B 0)) fun n p ↦ (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 : ℕ
x✝ : 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)