awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : eball x ε ⊆ s (ind x)
⊢ 0 < ε / 3

Tactic:
have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : eball x ε ⊆ s (ind x)
this : 0 < ε / 3
rcases :
  ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < ε / 3), ∃ (n : ℕ), eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)
⊢ ∃ (n : ℕ), eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)

Tactic:
rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩

Premises used: ENNReal.exists_inv_two_pow_lt, LT.lt.ne'
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : eball x ε ⊆ s (ind x)
this : 0 < ε / 3
n : ℕ
hn : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < ε / 3
⊢ ∃ (n : ℕ), eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)

Tactic:
⟨n, Subset.trans (eball_subset_eball ?_) hε⟩

Premises used: Metric.eball_subset_eball, Set.Subset.trans, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : eball x ε ⊆ s (ind x)
this : 0 < ε / 3
n : ℕ
hn : HPow.hPow (α := ℝ≥0∞) 2⁻¹ n < ε / 3
⊢ 3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ ε

Tactic:
simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le

Premises used: LT.lt.le, div_eq_mul_inv, mul_comm, ENNReal.mul_lt_of_lt_div
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
obtain : ∀ (n : ℕ) (hn : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)), ∃ (n : ℕ) (i : ι), x ∈ D n i
⊢ ∃ (n : ℕ) (i : ι), x ∈ D n i

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, eball x (3 * 2⁻¹ ^ n) ⊆ s (ind x) := by
      -- This proof takes 5 lines because we can't import `specific_limits` here
      rcases EMetric.isOpen_iff.1 (ho <| ind x) x (mem_ind x) with ⟨ε, ε0, hε⟩
      have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
      rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩
      refine ⟨n, Subset.trans (eball_subset_eball ?_) hε⟩
      simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
n : ℕ
hn : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)
by_contra! : ∀ (h : ∀ (n : ℕ) (i : ι), x ∉ D n i), False
⊢ ∃ (n : ℕ) (i : ι), x ∈ D n i

Tactic:
by_contra! h
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
n : ℕ
hn : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)
h : ∀ (n : ℕ) (i : ι), x ∉ D n i
apply : x ∈ D n (ind x)
⊢ False

Tactic:
apply h n (ind x)
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
n : ℕ
hn : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)
h : ∀ (n : ℕ) (i : ι), x ∉ D n i
⊢ x ∈ D n (ind x)

Tactic:
memD.2 ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_eball_self (pow_pos _)⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Metric.mem_eball_self, rfl
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
x : α
n : ℕ
hn : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s (ind x)
h : ∀ (n : ℕ) (i : ι), x ∉ D n i
⊢ x ∈ D n (ind x)

Tactic:
exact memD.2 ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_eball_self (pow_pos _)⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Metric.mem_eball_self, rfl
-- Module: Mathlib.Topology.EMetricSpace.Paracompact
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
⊢ ∀ (x : α), ∃ (n : ℕ) (i : ι), x ∈ D n i

Tactic:
have Dcov (x) : ∃ n i, x ∈ D n i := by
    obtain ⟨n, hn⟩ : ∃ n : ℕ, eball x (3 * 2⁻¹ ^ n) ⊆ s (ind x) := by
      -- This proof takes 5 lines because we can't import `specific_limits` here
      rcases EMetric.isOpen_iff.1 (ho <| ind x) x (mem_ind x) with ⟨ε, ε0, hε⟩
      have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
      rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩
      refine ⟨n, Subset.trans (eball_subset_eball ?_) hε⟩
      simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le
    by_contra! h
    apply h n (ind x)
    exact memD.2 ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_eball_self (pow_pos _)⟩