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
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 : ℕ
refine : ∀ᶠ (x : ℕ) in atTop, c x ∈ closedEBall (c n) (r n)
⊢ y ∈ closedEBall (c n) (r n)

Tactic:
refine isClosed_closedEBall.mem_of_tendsto ylim ?_

Premises used: IsClosed.mem_of_tendsto, Metric.isClosed_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
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)

Tactic:
(Filter.eventually_ge_atTop n).mono fun m hm => ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop
-- 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 : ℕ
refine : ∀ (m : ℕ) (hm : n ≤ m), c m ∈ closedEBall (c n) (r n)
⊢ ∀ᶠ (x : ℕ) in atTop, c x ∈ closedEBall (c n) (r n)

Tactic:
refine (Filter.eventually_ge_atTop n).mono fun m hm => ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop
-- 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 m : ℕ
hm : n ≤ m
⊢ c m ∈ closedEBall (c n) (r n)

Tactic:
I n m hm mem_closedEBall_self

Premises used: Metric.mem_closedEBall_self
-- 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 m : ℕ
hm : n ≤ m
⊢ c m ∈ closedEBall (c n) (r n)

Tactic:
exact I n m hm mem_closedEBall_self

Premises used: Metric.mem_closedEBall_self
-- 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:
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
-- 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)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
h : ∀ (i : ℕ), y ∈ f i
h₁ : y ∈ closedEBall x ε
⊢ (∀ (i : ℕ), y ∈ f i) ∧ y ∈ closedEBall x ε

Tactic:
constructor
-- 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)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
n : ℕ
⊢ 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
-- 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_1 : 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 : ℕ
this : closedEBall (c (n + 1)) (r (n + 1)) ⊆ f n
⊢ y ∈ f n

Tactic:
this (yball (n + 1))

Premises used: HAdd.hAdd, 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
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_1 : 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 : ℕ
this : closedEBall (c (n + 1)) (r (n + 1)) ⊆ f n
⊢ y ∈ f n

Tactic:
exact this (yball (n + 1))

Premises used: HAdd.hAdd, 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
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)
⊢ edist y x ≤ ε

Tactic:
le_trans (yball 0) (min_le_left _ _)

Premises used: min_le_left, OfNat.ofNat, le_trans
-- 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)
yball : ∀ (n : ℕ), y ∈ closedEBall (c n) (r n)
⊢ edist y x ≤ ε

Tactic:
exact le_trans (yball 0) (min_le_left _ _)

Premises used: min_le_left, le_trans
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
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:
simp [sInter_empty]

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Baire.Lemmas
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.insert a s_1, IsOpen[inst] t
hd : ∀ t ∈ Insert.insert a s_1, Dense t
insert : ∀ (hd : Dense a ∧ ∀ x ∈ s_1, Dense x), Dense (a ∩ ⋂₀ s_1)
⊢ Dense (⋂₀ Insert.insert a s_1)

Tactic:
simp only [sInter_insert, forall_mem_insert] at hd ⊢

Premises used: Set.forall_mem_insert, Set.sInter_insert
-- Module: Mathlib.Topology.Baire.Lemmas
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)

Tactic:
hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))

Premises used: Dense.inter_of_isOpen_right, And.left, Set.Finite.isOpen_sInter, Or.inr
-- Module: Mathlib.Topology.Baire.Lemmas
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.insert a s_1, IsOpen[inst] t
hd : Dense a ∧ ∀ x ∈ s_1, Dense x
insert : Dense (⋂₀ s_1)
⊢ Dense (a ∩ ⋂₀ s_1)

Tactic:
refine hd.1.inter_of_isOpen_right ?_ (hsf.isOpen_sInter (fun y hy => ho y (Or.inr hy)))

Premises used: Dense.inter_of_isOpen_right, And.left, Set.Finite.isOpen_sInter, Or.inr
-- Module: Mathlib.Topology.Baire.Lemmas
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 (⋂₀ s_1)

Tactic:
ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)

Premises used: And.right, Or.inr
-- Module: Mathlib.Topology.Baire.Lemmas
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 (⋂₀ s_1)

Tactic:
exact ih ((fun y hy => ho y (Or.inr hy))) (fun y hy => hd.2 y hy)

Premises used: And.right, Or.inr
-- Module: Mathlib.Topology.Baire.Lemmas
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) (⋂₀ ∅)
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.insert a s, IsOpen[inst] t) (hd : ∀ t ∈ Insert.insert a s, Dense t), Dense (⋂₀ Insert.insert a s)
⊢ Dense (⋂₀ 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)

Premises used: Set.forall_mem_insert, Set.sInter_empty, Set.sInter_insert, Insert.insert
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Finite X
f : ℕ → Set X
h : ∀ (n : ℕ), IsOpen[inst] (f n)
h_1 : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, IsOpen[inst] t

Tactic:
grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Finite X
f : ℕ → Set X
h : ∀ (n : ℕ), IsOpen[inst] (f n)
h_1 : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, Dense t

Tactic:
grind
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst] (f n)
hd : ∀ (n : ℕ), Dense (f n)
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)

Tactic:
BaireSpace.baire_property f ho hd

Premises used: BaireSpace.baire_property
-- Module: Mathlib.Topology.Baire.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : BaireSpace X
s : Set X
hG : IsGδ s
hd : Dense s
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)
⊢ BaireSpace.{u_1} (↑s : Type u_1)

Tactic:
constructor
-- Module: Mathlib.Topology.Baire.Lemmas
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)
⊢ ∃ (V : ℕ → Set X), (∀ (n : ℕ), IsOpen[inst] (V n)) ∧ s = ⋂ (n : ℕ), V n

Tactic:
eq_iInter_nat hG

Premises used: IsGδ.eq_iInter_nat
-- Module: Mathlib.Topology.Baire.Lemmas
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)
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)
⊢ 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

Premises used: IsGδ.eq_iInter_nat