awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
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
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have this : CauchySeq c
Tactic: have : CauchySeq c := cauchySeq_of_edist_le_geometric_two _ ENNReal.one_ne_top cdist
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have rcases : ∀ (y : X) (ylim : Tendsto c atTop (nhds y)),
  ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
Tactic: rcases cauchySeq_tendsto_of_complete this with ⟨y, ylim⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have h : Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
⊢ Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have h : (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε
Tactic: simp only [Set.mem_iInter]
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
have refine_1 : closedEBall (c n) (r n) ⊆ closedEBall (c n) (r n)
Tactic: refine Nat.le_induction ?_ fun m _ h => ?_
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
⊢ ∀ m ≥ n, closedEBall (c m) (r m) ⊆ closedEBall (c n) (r n)
have 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)
Tactic: refine Nat.le_induction ?_ fun m _ h => ?_
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
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 : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε
have I : ∀ (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)
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
have refine : ∀ᶠ (x : ℕ) in atTop, c x ∈ closedEBall (c n) (r n)
Tactic: refine isClosed_closedEBall.mem_of_tendsto ylim ?_
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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 : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, c x ∈ closedEBall (c n) (r n)
have refine : ∀ (m : ℕ) (hm : n ≤ m), c m ∈ closedEBall (c n) (r n)
Tactic: refine (Filter.eventually_ge_atTop n).mono fun m hm => ?_
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
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)
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε
have yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
Tactic: have yball : ∀ n, y ∈ closedEBall (c n) (r n) := by
    intro n
    refine isClosed_closedEBall.mem_of_tendsto ylim ?_
    refine (Filter.eventually_ge_atTop n).mono fun m hm => ?_
    exact I n m hm mem_closedEBall_self
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε
have h : ∀ (i : ℕ), y ∈ f i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
h : ∀ (i : ℕ), y ∈ f i
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε
have h₁ : y ∈ closedEBall x ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
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)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
n : ℕ
⊢ y ∈ f n
have this₁ : closedEBall (c (n + 1)) (r (n + 1)) ⊆ f n
Tactic: have : closedEBall (c (n + 1)) (r (n + 1)) ⊆ f n :=
      Subset.trans (incl n) inter_subset_right
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
a : Set X
s_1 : Set (Set X)
ha : a ∉ s_1
hsf : s_1.Finite
ih : ∀ (ho : ∀ t ∈ s_1, IsOpen[inst] t) (hd : ∀ t ∈ s_1, Dense t), Dense (⋂₀ s_1)
ho : ∀ t ∈ insert a s_1, IsOpen[inst] t
hd : ∀ t ∈ insert a s_1, Dense t
⊢ Dense (⋂₀ insert a s_1)
have insert : ∀ (hd : Dense a ∧ ∀ x ∈ s_1, Dense x), Dense (a ∩ ⋂₀ s_1)
Tactic: simp only [sInter_insert, forall_mem_insert] at hd ⊢
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
a : Set X
s_1 : Set (Set X)
ha : a ∉ s_1
hsf : s_1.Finite
ih : ∀ (ho : ∀ t ∈ s_1, IsOpen[inst] t) (hd : ∀ t ∈ s_1, Dense t), Dense (⋂₀ s_1)
ho : ∀ t ∈ insert a s_1, IsOpen[inst] t
hd : Dense a ∧ ∀ x ∈ s_1, Dense x
⊢ Dense (a ∩ ⋂₀ s_1)
have insert : Dense (⋂₀ s_1)
Tactic: refine hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t
hd : ∀ t ∈ s, Dense t
⊢ Dense (⋂₀ s)
have empty : ∀ (ho : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t)
  (hd : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → Dense t), Dense.{u_1} (X := X) (⋂₀ ∅)
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp [sInter_empty]
  | insert ha hsf ih =>
    simp only [sInter_insert, forall_mem_insert] at hd ⊢
    refine hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))
    exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)
Cleared hypotheses: hs, ho, hd
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
hs : s.Finite
ho : ∀ t ∈ s, IsOpen[inst] t
hd : ∀ t ∈ s, Dense t
empty :
  ∀ (ho : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t)
    (hd : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → Dense t), Dense.{u_1} (X := X) (⋂₀ ∅)
⊢ Dense (⋂₀ s)
have insert : ∀ {a : Set X} {s : Set (Set X)} (ha : a ∉ s) (hsf : s.Finite)
  (ih : ∀ (ho : ∀ t ∈ s, IsOpen[inst] t) (hd : ∀ t ∈ s, Dense t), Dense (⋂₀ s)) (ho : ∀ t ∈ insert a s, IsOpen[inst] t)
  (hd : ∀ t ∈ insert a s, Dense t), Dense (⋂₀ insert a s)
Tactic: induction s, hs using Set.Finite.induction_on with
  | empty => simp [sInter_empty]
  | insert ha hsf ih =>
    simp only [sInter_insert, forall_mem_insert] at hd ⊢
    refine hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))
    exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)
Cleared hypotheses: hs, ho, hd
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
⊢ BaireSpace.{u_1} (↑s : Type u_1)
have baire_property : ∀ (f : ℕ → Set (↑s : Type u_1)),
  (∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)) →
    (∀ (n : ℕ), Dense (f n)) → Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Baire.Lemmas (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
f : ℕ → Set (↑s : Type u_1)
hof : ∀ (n : ℕ), IsOpen[instTopologicalSpaceSubtype] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
⊢ Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
have baire_property : ∀ (V : ℕ → Set X) (hV : (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n),
  Dense.{u_1} (X := (↑s : Type u_1)) (⋂ (n : ℕ), f n)
Tactic: obtain ⟨V, hV⟩ : ∃ V : ℕ → Set X, (∀ n, IsOpen (V n)) ∧ s = ⋂ n, V n := eq_iInter_nat hG