awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
inl :
  ∀ (hJ : IsEmpty.{u_1 + 1} ↥J),
    ∃ K ⊆ J ×ˢ J,
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have inl₁ : ∀ (hJ : Nonempty.{u_1 + 1} ↥J),
  ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
Tactic: rcases isEmpty_or_nonempty J with hJ | hJ
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (hypothesis)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : IsEmpty.{u_1 + 1} ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have hJ₁ : J = ∅
Tactic: simp only [Finset.isEmpty_coe_sort] at hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ ∃ (x₀ : T), J = {x₀}
have rw : #J = 1
Tactic: rw [← Finset.card_eq_one]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ #J = 1
have refine_1 : #J ≤ 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
refine_1 : #J ≤ 1
⊢ #J = 1
have refine_2 : 1 ≤ #J
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
this : LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1
⊢ #J ≤ 1
have norm_cast : ∀ (this : #J ≤ 1), #J ≤ 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ #J ≤ 1
have refine_1 : LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1
Tactic: suffices (#J : ENNReal) ≤ 1 by norm_cast at this
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ LE.le (α := ℝ≥0∞) (↑(#J) : ℝ≥0∞) 1
have refine_1 : a ^ n ≤ 1
Tactic: refine hJ_card.trans ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
| 1
have rw : HPow.hPow (α := ℝ≥0∞) 1 n
Tactic: rw [← one_pow n]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ a ^ n ≤ 1
have refine_1 : a ^ n ≤ HPow.hPow (α := ℝ≥0∞) 1 n
Tactic: conv_rhs => rw [← one_pow n]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ 1 ≤ #J
have refine_2 : J.Nonempty
Tactic: rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty.{u_1 + 1} ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have inl : ∀ (x₀ : T) (hJ_card : (↑(Finset.card (α := T) {x₀}) : ℝ≥0∞) ≤ a ^ n) (hJ : Nonempty.{u_1 + 1} ↥{x₀}),
  ∃ K ⊆ SProd.sprod (α := Finset T) (β := Finset T) {x₀} {x₀},
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(Finset.card (α := T) {x₀}) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥{x₀}), ⨆ (t : { t : ↥{x₀} // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥{x₀}) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
Tactic: obtain ⟨x₀, rfl⟩ : ∃ x₀, J = {x₀} := by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]
Cleared hypotheses: J, hJ_card, hJ
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have inl : ∀ (ha1 : a ≤ 1),
  ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
Tactic: classical
  rcases le_or_gt a 1 with ha1 | ha1
  · rcases isEmpty_or_nonempty J with hJ | hJ
    · simp only [Finset.isEmpty_coe_sort] at hJ
      simp [hJ]
    obtain ⟨x₀, rfl⟩ : ∃ x₀, J = {x₀} := by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]
    simp_all
  · exact ⟨pairSet J a c, pairSet_subset, card_pairSet_le ha1,
      fun _ _ ↦ edist_le_of_mem_pairSet ha1 hJ_card, iSup_edist_pairSet ha1⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.PairReduction (goal)
Goal:
T : Type u_1
inst : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : (↑(#J) : ℝ≥0∞) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst_1 : PseudoEMetricSpace E
inl :
  ∀ (ha1 : a ≤ 1),
    ∃ K ⊆ J ×ˢ J,
      (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
        (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
          ∀ (f : T → E),
            ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
              HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
⊢ ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
have inr : ∀ (ha1 : 1 < a),
  ∃ K ⊆ J ×ˢ J,
    (↑(#K) : ℝ≥0∞) ≤ a * (↑(#J) : ℝ≥0∞) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ (↑n : ℝ≥0∞) * c) ∧
        ∀ (f : T → E),
          ⨆ (s : ↥J), ⨆ (t : { t : ↥J // edist s t ≤ c }), edist (f (↑s : T)) (f (↑(↑t : ↥J) : T)) ≤
            HMul.hMul (α := ℝ≥0∞) 2 (⨆ (p : ↥K), edist (f (↑p : T × T).1) (f (↑p : T × T).2))
Tactic: classical
  rcases le_or_gt a 1 with ha1 | ha1
  · rcases isEmpty_or_nonempty J with hJ | hJ
    · simp only [Finset.isEmpty_coe_sort] at hJ
      simp [hJ]
    obtain ⟨x₀, rfl⟩ : ∃ x₀, J = {x₀} := by
      rw [← Finset.card_eq_one]
      refine le_antisymm ?_ ?_
      · suffices (#J : ENNReal) ≤ 1 by norm_cast at this
        refine hJ_card.trans ?_
        conv_rhs => rw [← one_pow n]
        exact ENNReal.pow_le_pow_left ha1
      · rwa [Finset.one_le_card, ← Finset.nonempty_coe_sort]
    simp_all
  · exact ⟨pairSet J a c, pairSet_subset, card_pairSet_le ha1,
      fun _ _ ↦ edist_le_of_mem_pairSet ha1 hJ_card, iSup_edist_pairSet ha1⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ ParacompactSpace α
have pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
Tactic: have pow_pos : ∀ k : ℕ, (0 : ℝ≥0∞) < 2⁻¹ ^ k := fun k =>
    ENNReal.pow_pos (ENNReal.inv_pos.2 ENNReal.ofNat_ne_top) _
-- 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
⊢ ParacompactSpace α
have hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
Tactic: have hpow_le : ∀ {m n : ℕ}, m ≤ n → (2⁻¹ : ℝ≥0∞) ^ n ≤ 2⁻¹ ^ m := @fun m n h =>
    pow_le_pow_right_of_le_one' (ENNReal.inv_le_one.2 ENNReal.one_lt_two.le) h
-- 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
⊢ ParacompactSpace α
have h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
Tactic: have h2pow : ∀ n : ℕ, 2 * (2⁻¹ : ℝ≥0∞) ^ (n + 1) = 2⁻¹ ^ n := fun n => by
    simp [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel two_ne_zero ofNat_ne_top]
-- 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
⊢ ParacompactSpace α
have refine : ∀ (ι : Type u_1) (s : ι → Set α) (ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a))
  (hcov : Eq.{u_1 + 1} (α := Set α) (⋃ (a : ι), s a) univ),
  ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
Tactic: refine ⟨fun ι s ho hcov => ?_⟩
-- 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 : Eq.{u_1 + 1} (α := Set α) (⋃ (a : ι), s a) univ
⊢ ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
have hcov₁ : ∀ (x : α), ∃ (i : ι), x ∈ s i
Tactic: simp only [iUnion_eq_univ_iff] at hcov
Cleared hypotheses: hcov
-- 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
⊢ ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
have obtain : ∀ (w : LinearOrder ι) (wf : WellFoundedLT ι),
  ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
Tactic: obtain ⟨_, wf⟩ := exists_wellFoundedLT ι
-- 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} ⋯
⊢ ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
have mem_ind : ∀ (x : α), x ∈ s (ind x)
Tactic: have mem_ind (x) : x ∈ s (ind x) := wellFounded_lt.min_mem _ (hcov x)
-- 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)
⊢ ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
have notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
Tactic: have notMem_of_lt_ind {x i} (hlt : i < ind x) (hxi : x ∈ s i) : False :=
    wellFounded_lt.not_lt_min {i | x ∈ s i} hxi hlt
-- 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
⊢ ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
have hD : let 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);
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)
Tactic: set D : ℕ → ι → Set α := fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (hxs : ind x = i) (hb : eball x (3 * 2⁻¹ ^ n) ⊆ s i) (hlt :
        ∀ (m : ℕ) (H : m < n), ∀ (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n) with hD
-- 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)
⊢ ∃ (β : Type u_1) (t : β → Set α),
    (∀ (b : β), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (t b)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (b : β), t b) univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : ι), t b ⊆ s a
have 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)
Tactic: have Dn (n i) : D n i = ⋃ (x : α) (hxs : ind x = i) (hb : eball x (3 * 2⁻¹ ^ n) ⊆ s i)
      (hlt : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n) := by
    simp only [hD]
    rw [Nat.strongRecOn'_beta]
-- 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)
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
have rw : Membership.mem (γ := Set α)
    (⋃ (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))
    y ↔
  ∃ (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
Tactic: rw [Dn n i]