awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have refine_1 : 0 < min (min (δ / 2) r) (B (n + 1))
Tactic: refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
-- 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
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
refine_1 : 0 < min (min (δ / 2) r) (B (n + 1))
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have refine_2 : min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
Tactic: refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
-- 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
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
refine_1 : 0 < min (min (δ / 2) r) (B (n + 1))
refine_2 : min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have refine_3 : ∀ (z : X) (hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))), z ∈ closedEBall x δ
Tactic: refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
-- 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
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
refine_1 : 0 < min (min (δ / 2) r) (B (n + 1))
refine_2 : min (min (δ / 2) r) (B (n + 1)) ≤ B (n + 1)
refine_3 : ∀ (z : X) (hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))), z ∈ closedEBall x δ
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have refine_4 : ∀ (z : X) (hz : z ∈ closedEBall y (min (min (δ / 2) r) (B (n + 1)))), z ∈ f n
Tactic: refine ⟨y, min (min (δ / 2) r) (B (n + 1)), ?_, ?_, fun z hz => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
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
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
have 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
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 _ _))
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
have 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)
Tactic: choose! center radius Hpos HB Hball using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
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)
have refine : ∀ (x_1 : X) (ε : ℝ≥0∞) (εpos : 0 < ε), ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x_1 ε
Tactic: refine fun x => (mem_closure_iff_nhds_basis nhds_basis_closedEBall).2 fun ε εpos => ?_
-- 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
n : ℕ
⊢ 0 < r n
have zero : 0 < r 0
Tactic: induction n with
    | zero => exact lt_min εpos (Bpos 0)
    | succ n hn => exact Hpos n (c n) (r n) hn.ne'
Cleared hypotheses: n
-- 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
n : ℕ
zero : 0 < r 0
⊢ 0 < r n
have succ : ∀ (n : ℕ) (hn : 0 < r n), 0 < r (n + 1)
Tactic: induction n with
    | zero => exact lt_min εpos (Bpos 0)
    | succ n hn => exact Hpos n (c n) (r n) hn.ne'
Cleared hypotheses: n
-- 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
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have rpos : ∀ (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'
-- 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
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have r0 : ∀ (n : ℕ), r n ≠ 0
Tactic: have r0 : ∀ n, r n ≠ 0 := fun n => (rpos n).ne'
-- 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
n : ℕ
⊢ r n ≤ B n
have zero : r 0 ≤ B 0
Tactic: cases n with
    | zero => exact min_le_right _ _
    | succ n => exact HB n (c n) (r n) (r0 n)
Cleared hypotheses: n
-- 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
n : ℕ
zero : r 0 ≤ B 0
⊢ r n ≤ B n
have succ : ∀ (n : ℕ), r (n + 1) ≤ B (n + 1)
Tactic: cases n with
    | zero => exact min_le_right _ _
    | succ n => exact HB n (c n) (r n) (r0 n)
Cleared hypotheses: n
-- 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
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have rB : ∀ (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)
-- 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
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have incl : ∀ (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)
-- 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
n : ℕ
⊢ edist (c n) (c (n + 1)) ≤ B n
have rw : edist (c (n + 1)) (c n) ≤ B n
Tactic: rw [edist_comm]
-- 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
n : ℕ
⊢ edist (c (n + 1)) (c n) ≤ B n
have A : 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
-- 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
n : ℕ
A : c (n + 1) ∈ closedEBall (c (n + 1)) (r (n + 1))
⊢ edist (c (n + 1)) (c n) ≤ B n
have I : 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)
-- 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
⊢ ∃ (y : X), Membership.mem (γ := Set X) (⋂ (n : ℕ), f n) y ∧ y ∈ closedEBall x ε
have cdist : ∀ (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