awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
m : ℕ
hm : n + k + 1 ≤ m
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : eball z (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m) ⊆ s (ind z)
H : ∀ m_1 < m, ∀ (j : ι), z ∉ D m_1 j
hz : edist y z < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
⊢ Membership.mem (γ := Set α) ⊥ y
have this₁ : z ∉ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
Tactic: have : z ∉ eball x (2⁻¹ ^ k) := fun hz' => H n (by lia) i (hsub hz')
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
m : ℕ
hm : n + k + 1 ≤ m
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : eball z (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m) ⊆ s (ind z)
H : ∀ m_1 < m, ∀ (j : ι), z ∉ D m_1 j
hz : edist y z < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
this : z ∉ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
⊢ Membership.mem (γ := Set α) ⊥ y
have apply : z ∈ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
Tactic: apply this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
m : ℕ
hm : n + k + 1 ≤ m
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : eball z (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m) ⊆ s (ind z)
H : ∀ m_1 < m, ∀ (j : ι), z ∉ D m_1 j
hz : edist y z < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
this : z ∉ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) + HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have rw : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: rw [← two_mul, h2pow]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
m : ℕ
hm : n + k + 1 ≤ m
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : eball z (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m) ⊆ s (ind z)
H : ∀ m_1 < m, ∀ (j : ι), z ∉ D m_1 j
hz : edist y z < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
this : z ∉ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
rw : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
⊢ HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) + HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
have rw₁ : HPow.hPow (α := ℝ≥0∞) 2⁻¹ k = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: rw [← two_mul, h2pow]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this_1 : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
m : ℕ
hm : n + k + 1 ≤ m
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : eball z (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m) ⊆ s (ind z)
H : ∀ m_1 < m, ∀ (j : ι), z ∉ D m_1 j
hz : edist y z < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
this : z ∉ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
⊢ z ∈ eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k)
have edist : HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) + HPow.hPow (α := ℝ≥0∞) 2⁻¹ (k + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: calc
        edist z x ≤ edist y z + edist y x := edist_triangle_left _ _ _
        _ < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) := ENNReal.add_lt_add hz hyx
        _ ≤ 2⁻¹ ^ (k + 1) + 2⁻¹ ^ (k + 1) :=
          (add_le_add (hpow_le <| by lia) (hpow_le <| by lia))
        _ = 2⁻¹ ^ k := by rw [← two_mul, h2pow]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
⊢ Set.Finite.{u_1} (α := ℕ × ι) {i : ℕ × ι | ((fun (ni : ℕ × ι) ↦ D ni.1 ni.2) i ∩ B).Nonempty}
have Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
Tactic: have Hgt (m) (hm : n + k + 1 ≤ m) (i : ι) : Disjoint (D m i) B := by
      rw [disjoint_iff_inf_le]
      rintro y ⟨hym, hyx⟩
      rcases memD.1 hym with ⟨z, rfl, _hzi, H, hz⟩
      have : z ∉ eball x (2⁻¹ ^ k) := fun hz' => H n (by lia) i (hsub hz')
      apply this
      calc
        edist z x ≤ edist y z + edist y x := edist_triangle_left _ _ _
        _ < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) := ENNReal.add_lt_add hz hyx
        _ ≤ 2⁻¹ ^ (k + 1) + 2⁻¹ ^ (k + 1) :=
          (add_le_add (hpow_le <| by lia) (hpow_le <| by lia))
        _ = 2⁻¹ ^ k := by rw [← two_mul, h2pow]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
j₁ : ι
y : α
hyD : y ∈ D m j₁
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
⊢ j₁ = j₂
have by_contra : ∀ (h' : j₁ ≠ j₂), False
Tactic: by_contra h' : j₁ ≠ j₂
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ (i : ι), x ∈ s i
w : LinearOrder ι
wf : WellFoundedLT ι
ind : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Dcov : ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
j₁ : ι
y : α
hyD : y ∈ D m j₁
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
h' : j₁ ≠ j₂
⊢ False
have inr : ∀
  (this :
    ∀ ⦃j₁ : ι⦄ (y : α) (hyD : y ∈ D m j₁) (hyB : y ∈ B) ⦃j₂ : ι⦄ (z : α) (hzD : z ∈ D m j₂) (hzB : z ∈ B) (h' : j₁ ≠ j₂)
      (h : j₁ < j₂), False)
  (h : ¬j₁ < j₂), False
Tactic: wlog h : j₁ < j₂ generalizing j₁ j₂ y z