awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ edist x y ≤ edist (f x) (f y) * (↑K₁ : ℝ≥0∞)
have rw : edist x y ≤ (↑K₁ : ℝ≥0∞) * edist (f x) (f y)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε : ℝ≥0∞) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ (↑(ε / K₁) : ℝ≥0∞) < edist (f x) (f y)
have hmul : (↑ε : ℝ≥0∞) < edist (f x) (f y) * (↑K₁ : ℝ≥0∞)
Tactic: have hmul : (↑ε : ℝ≥0∞) < edist (f x) (f y) * ↑K₁ :=
    lt_of_lt_of_le (hs hx hy (by grind)) (by rw [mul_comm]; exact hf x y)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
h : AreSeparated s t
h' : AreSeparated s' t
⊢ AreSeparated (s ∪ s') t
have rcases : ∀ (r : ℝ≥0∞) (r0 : r ≠ 0) (hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y) (r' : ℝ≥0∞) (r0' : r' ≠ 0)
  (hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y), AreSeparated (s ∪ s') t
Tactic: rcases h, h' with ⟨⟨r, r0, hr⟩, ⟨r', r0', hr'⟩⟩
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t
have refine_1 : min r r' ≠ 0
Tactic: refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
refine_1 : min r r' ≠ 0
⊢ AreSeparated (s ∪ s') t
have refine_2 : ∀ (x : X) (hx : x ∈ s ∪ s') (y : X) (hy : y ∈ t), x ∈ s → min r r' ≤ edist x y
Tactic: refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
refine_1 : min r r' ≠ 0
refine_2 : ∀ (x : X) (hx : x ∈ s ∪ s') (y : X) (hy : y ∈ t), x ∈ s → min r r' ≤ edist x y
⊢ AreSeparated (s ∪ s') t
have refine_3 : ∀ (x : X) (hx : x ∈ s ∪ s') (y : X) (hy : y ∈ t), x ∈ s' → min r r' ≤ edist x y
Tactic: refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
r : ℝ≥0∞
r0 : r ≠ 0
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
r' : ℝ≥0∞
r0' : r' ≠ 0
hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y
⊢ min r r' ≠ 0
have refine_1 : ∀ (r0 : 0 < r) (hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y) (r' : ℝ≥0∞) (r0' : 0 < r')
  (hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y), 0 < min r r'
Tactic: rw [← pos_iff_ne_zero] at r0 r0' ⊢
Cleared hypotheses: r0, hr, r', r0', hr'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
hI : AreSeparated (⋃ i ∈ s_1, s i) t ↔ ∀ i ∈ s_1, AreSeparated (s i) t
⊢ AreSeparated (⋃ i ∈ insert a s_1, s i) t ↔ ∀ i ∈ insert a s_1, AreSeparated (s i) t
have insert : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ ∀ i ∈ insert a s_1, AreSeparated (s i) t
Tactic: rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
hI : AreSeparated (⋃ i ∈ s_1, s i) t ↔ ∀ i ∈ s_1, AreSeparated (s i) t
insert : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
⊢ AreSeparated (⋃ i ∈ Insert.insert a s_1, s i) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
have insert₁ : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ AreSeparated (s a) t ∧ ∀ x ∈ s_1, AreSeparated (s x) t
Tactic: rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
hI : AreSeparated (⋃ i ∈ s_1, s i) t ↔ ∀ i ∈ s_1, AreSeparated (s i) t
insert : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
insert₁ : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ AreSeparated (s a) t ∧ ∀ x ∈ s_1, AreSeparated (s x) t
⊢ AreSeparated (⋃ i ∈ Insert.insert a s_1, s i) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
have insert₂ : AreSeparated (s a) t ∧ AreSeparated (⋃ x ∈ s_1, s x) t ↔ AreSeparated (s a) t ∧ ∀ x ∈ s_1, AreSeparated (s x) t
Tactic: rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
hI : AreSeparated (⋃ i ∈ s_1, s i) t ↔ ∀ i ∈ s_1, AreSeparated (s i) t
insert : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
insert₁ : AreSeparated (s a ∪ ⋃ x ∈ s_1, s x) t ↔ AreSeparated (s a) t ∧ ∀ x ∈ s_1, AreSeparated (s x) t
insert₂ :
  AreSeparated (s a) t ∧ AreSeparated (⋃ x ∈ s_1, s x) t ↔ AreSeparated (s a) t ∧ ∀ x ∈ s_1, AreSeparated (s x) t
⊢ AreSeparated (⋃ i ∈ Insert.insert a s_1, s i) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
have insert₃ : (AreSeparated (s a) t ∧ ∀ i ∈ s_1, AreSeparated (s i) t) ↔ AreSeparated (s a) t ∧ ∀ x ∈ s_1, AreSeparated (s x) t
Tactic: rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
hI : I.Finite
s : ι → Set X
t : Set X
⊢ AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t
have empty : AreSeparated (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i) t ↔
  ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → AreSeparated (s i) t
Tactic: induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hI => rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.MetricSeparated (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
hI : I.Finite
s : ι → Set X
t : Set X
empty :
  AreSeparated (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i) t ↔
    ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → AreSeparated (s i) t
⊢ AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t
have insert : ∀ {a : ι} {s_1 : Set ι},
  a ∉ s_1 →
    s_1.Finite →
      ∀ (hI : AreSeparated (⋃ i ∈ s_1, s i) t ↔ ∀ i ∈ s_1, AreSeparated (s i) t),
        AreSeparated (⋃ i ∈ insert a s_1, s i) t ↔ ∀ i ∈ insert a s_1, AreSeparated (s i) t
Tactic: induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hI => rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i
have apply : {x_1 : ℝ≥0∞ × X |
    Membership.mem (γ := Set (ℝ≥0∞ × X)) (Prod.snd ⁻¹' ⋂ (i : ι), ⋂ (_ : x ∉ K i), (K i)ᶜ) x_1 →
      Membership.mem (γ := Set (ℝ≥0∞ × X))
        {x_2 : ℝ≥0∞ × X |
          Membership.mem (γ := Set (ℝ≥0∞ × X))
              {x_3 : ℝ≥0∞ × X |
                (fun (x_4 : ℝ≥0∞ × X) ↦
                    ∀ (i : ι), Membership.mem (γ := Set ι) {b : ι | x ∈ K b} i → closedEBall x_4.2 x_4.1 ⊆ U i)
                  x_3}
              x_2 →
            Membership.mem (γ := Set (ℝ≥0∞ × X))
              {x : ℝ≥0∞ × X | (fun (p : ℝ≥0∞ × X) ↦ ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i) x} x_2}
        x_1} ∈
  SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x)
Tactic: apply mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
      (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
⊢ {x_1 : ℝ≥0∞ × X |
      Membership.mem (γ := Set (ℝ≥0∞ × X)) (Prod.snd ⁻¹' ⋂ (i : ι), ⋂ (_ : x ∉ K i), (K i)ᶜ) x_1 →
        Membership.mem (γ := Set (ℝ≥0∞ × X))
          {x_2 : ℝ≥0∞ × X |
            Membership.mem (γ := Set (ℝ≥0∞ × X))
                {x_3 : ℝ≥0∞ × X |
                  (fun (x_4 : ℝ≥0∞ × X) ↦
                      ∀ (i : ι), Membership.mem (γ := Set ι) {b : ι | x ∈ K b} i → closedEBall x_4.2 x_4.1 ⊆ U i)
                    x_3}
                x_2 →
              Membership.mem (γ := Set (ℝ≥0∞ × X))
                {x : ℝ≥0∞ × X | (fun (p : ℝ≥0∞ × X) ↦ ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i) x} x_2}
          x_1} ∈
    SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x)
have h : ∀ (a : ℝ≥0∞ × X),
  Membership.mem (γ := Set (ℝ≥0∞ × X))
    {x_1 : ℝ≥0∞ × X |
      Membership.mem (γ := Set (ℝ≥0∞ × X)) (Prod.snd ⁻¹' ⋂ (i : ι), ⋂ (_ : x ∉ K i), (K i)ᶜ) x_1 →
        Membership.mem (γ := Set (ℝ≥0∞ × X))
          {x_2 : ℝ≥0∞ × X |
            Membership.mem (γ := Set (ℝ≥0∞ × X))
                {x_3 : ℝ≥0∞ × X |
                  (fun (x_4 : ℝ≥0∞ × X) ↦
                      ∀ (i : ι), Membership.mem (γ := Set ι) {b : ι | x ∈ K b} i → closedEBall x_4.2 x_4.1 ⊆ U i)
                    x_3}
                x_2 →
              Membership.mem (γ := Set (ℝ≥0∞ × X))
                {x : ℝ≥0∞ × X | (fun (p : ℝ≥0∞ × X) ↦ ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i) x} x_2}
          x_1}
    a
Tactic: apply univ_mem'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
r : ℝ≥0∞
y : X
hxy : Membership.mem (γ := Set (ℝ≥0∞ × X)) (Prod.snd ⁻¹' ⋂ (i : ι), ⋂ (_ : x ∉ K i), (K i)ᶜ) (r, y)
hyU :
  Membership.mem (γ := Set (ℝ≥0∞ × X))
    {x_1 : ℝ≥0∞ × X |
      (fun (x_2 : ℝ≥0∞ × X) ↦
          ∀ (i : ι), Membership.mem (γ := Set ι) {b : ι | x ∈ K b} i → closedEBall x_2.2 x_2.1 ⊆ U i)
        x_1}
    (r, y)
i : ι
hi : (r, y).2 ∈ K i
⊢ closedEBall (r, y).2 (r, y).1 ⊆ U i
have hxy₁ : ∀ (i : ι), y ∈ K i → x ∈ K i
Tactic: simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i
have suffices : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
Tactic: suffices ∀ i, x ∈ K i → ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i by
    apply mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
      (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
    apply univ_mem'
    rintro ⟨r, y⟩ hxy hyU i hi
    simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
    exact hyU _ (hxy _ hi)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
have rcases : ∀ (R : ℝ≥0∞) (hR₀ : 0 < R) (hR : closedEBall x R ⊆ U i),
  ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
Tactic: rcases nhds_basis_closedEBall.mem_iff.1 ((hU i).mem_nhds <| hKU i hi) with ⟨R, hR₀, hR⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedEBall x R ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
have rcases : ∀ (r : ℝ≥0) (hr₀ : 0 < (↑r : ℝ≥0∞)) (hrR : (↑r : ℝ≥0∞) < R),
  ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.mp hR₀ with ⟨r, hr₀, hrR⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedEBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ≥0∞)
hrR : (↑r : ℝ≥0∞) < R
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ U i
have h : ∀ (p : ℝ≥0∞ × X) (hp : p ∈ SProd.sprod (α := Set ℝ≥0∞) {x : ℝ≥0∞ | x < (↑r : ℝ≥0∞)} (closedEBall x (R - (↑r : ℝ≥0∞))))
  ⦃z : X⦄ (hz : z ∈ closedEBall p.2 p.1), z ∈ U i
Tactic: filter_upwards [prod_mem_prod (eventually_lt_nhds hr₀)
      (closedEBall_mem_nhds x (tsub_pos_iff_lt.2 hrR))] with p hp z hz
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedEBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ≥0∞)
hrR : (↑r : ℝ≥0∞) < R
p : ℝ≥0∞ × X
hp : p ∈ SProd.sprod (α := Set ℝ≥0∞) {x : ℝ≥0∞ | x < (↑r : ℝ≥0∞)} (closedEBall x (R - (↑r : ℝ≥0∞)))
z : X
hz : z ∈ closedEBall p.2 p.1
⊢ z ∈ U i
have h : z ∈ closedEBall x R
Tactic: apply hR
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∃ (r : ℝ),
    ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
have this : ∀ᶠ (x_1 : ℝ) in 𝓝 0,
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
Tactic: have := (ENNReal.continuous_ofReal.tendsto' 0 0 ENNReal.ofReal_zero).eventually
    (eventually_nhds_zero_forall_closedEBall_subset hK hU hKU hfin x).curry
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
⊢ ∃ (r : ℝ),
    ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
have rcases : ∀ (r : ℝ) (hr0 : 0 < r)
  (hr :
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i),
  ∃ (r : ℝ),
    ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
Tactic: rcases this.exists_gt with ⟨r, hr0, hr⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
⊢ ∃ (r : ℝ),
    ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
have refine : ∀ (y : X)
  (hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i),
  r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
Tactic: refine ⟨r, hr.mono fun y hy => ⟨hr0, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
have rwa : Membership.mem (γ := Set ℝ≥0∞) (⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}) (ENNReal.ofReal r)
Tactic: rwa [mem_preimage, mem_iInter₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
rwa : Membership.mem (γ := Set ℝ≥0∞) (⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}) (ENNReal.ofReal r)
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}
have rwa₁ : ∀ (i : ι) (j : y ∈ K i), Membership.mem (γ := Set ℝ≥0∞) {r : ℝ≥0∞ | closedEBall y r ⊆ U i} (ENNReal.ofReal r)
Tactic: rwa [mem_preimage, mem_iInter₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
have rcases : ∀ (δ : C(X, ℝ)) (hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ))
  (hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : X) → ℝ) x)) ⊆ U i),
  ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
Tactic: rcases exists_continuous_real_forall_closedEBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.PartitionOfUnity (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : X) → ℝ) x)) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
have lift : ∀ (δ : C(X, ℝ≥0)) (hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x : ℝ))
  (hδ :
    ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x)) ⊆ U i),
  ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
Tactic: lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le
Cleared hypotheses: δ, hδ₀, hδ