awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t s' : Set X
⊢ AreSeparated (s ∪ s') t ↔ AreSeparated s t ∧ AreSeparated s' t

Tactic:
⟨fun h => ⟨h.mono_left subset_union_left, h.mono_left subset_union_right⟩, fun h =>
    h.1.union_left h.2⟩

Premises used: Metric.AreSeparated.mono_left, Set.subset_union_right, Set.subset_union_left, And.right, And.left, Metric.AreSeparated.union_left, And.intro, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t t' : Set X
h : AreSeparated s t
h' : AreSeparated s t'
⊢ AreSeparated s (t ∪ t')

Tactic:
(h.symm.union_left h'.symm).symm

Premises used: Metric.AreSeparated.symm, Metric.AreSeparated.union_left
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
s t t' : Set X
⊢ AreSeparated s (t ∪ t') ↔ AreSeparated s t ∧ AreSeparated s t'

Tactic:
comm.trans <| union_left_iff.trans <| and_congr comm comm

Premises used: Metric.AreSeparated.comm, Iff.trans, Metric.AreSeparated.union_left_iff, and_congr
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
⊢ AreSeparated (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i) t ↔
    ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → AreSeparated (s i) t

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
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
insert₃ insert₄ :
  (AreSeparated (s a) t ∧ ∀ i ∈ s_1, AreSeparated (s i) 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

Tactic:
rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]

Premises used: Set.forall_mem_insert, Set.biUnion_insert, Metric.AreSeparated.union_left_iff
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
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
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.insert a s_1, s i) t ↔ ∀ i ∈ Insert.insert a s_1, AreSeparated (s i) t
⊢ AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ 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]

Premises used: Set.forall_mem_insert, Set.biUnion_insert, Insert.insert, Metric.AreSeparated.union_left_iff
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
hI : I.Finite
s : Set X
t : ι → Set X
⊢ AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

Tactic:
simpa only [@comm _ _ s] using finite_iUnion_left_iff hI

Premises used: Metric.AreSeparated.comm, Metric.AreSeparated.finite_iUnion_left_iff
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Finset ι
s : ι → Set X
t : Set X
⊢ AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t

Tactic:
finite_iUnion_left_iff I.finite_toSet

Premises used: Finset.finite_toSet, Metric.AreSeparated.finite_iUnion_left_iff
-- Module: Mathlib.Topology.MetricSpace.MetricSeparated
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ι : Type u_3
I : Finset ι
s : Set X
t : ι → Set X
⊢ AreSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, AreSeparated s (t i)

Tactic:
finite_iUnion_right_iff I.finite_toSet

Premises used: Metric.AreSeparated.finite_iUnion_right_iff, Finset.finite_toSet
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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)
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), ∀ (i : ι), p.2 ∈ K i → closedEBall p.2 p.1 ⊆ U i

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)) _)

Premises used: Iff.mpr, Filter.mp_mem, LocallyFinite.iInter_compl_mem_nhds, LocallyFinite.point_finite, Filter.eventually_all_finite, Filter.tendsto_snd
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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
⊢ {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 univ_mem'

Premises used: Filter.univ_mem'
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
⊢ ∀ (i : ι), y ∈ K i → x ∈ K i

Tactic:
simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy

Premises used: Set.mem_iInter, Set.mem_compl_iff, Set.mem_preimage, not_imp_not
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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
hxy : ∀ (i : ι), y ∈ K i → x ∈ K i
⊢ closedEBall (r, y).2 (r, y).1 ⊆ U i

Tactic:
hyU _ (hxy _ hi)
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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
hxy : ∀ (i : ι), y ∈ K i → x ∈ K i
⊢ closedEBall (r, y).2 (r, y).1 ⊆ U i

Tactic:
exact hyU _ (hxy _ hi)
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
suffices :
  ∀ (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

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)
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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
⊢ ∀ᶠ (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⟩

Premises used: Filter.HasBasis.mem_iff, IsOpen.mem_nhds, Iff.mp, Metric.nhds_basis_closedEBall
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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
⊢ ∀ᶠ (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⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in SProd.sprod (α := Filter ℝ≥0∞) (𝓝 0) (𝓝 x), closedEBall p.2 p.1 ⊆ 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

Premises used: Metric.closedEBall_mem_nhds, Iff.mpr, tsub_pos_iff_lt, eventually_lt_nhds, Filter.prod_mem_prod
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
h : z ∈ closedEBall x R
⊢ z ∈ U i

Tactic:
apply hR
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
⊢ edist z x ≤ edist z p.2 + edist p.2 x

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
⊢ edist z p.2 + edist p.2 x ≤ p.1 + (R - p.1)

Tactic:
add_le_add hz <| le_trans hp.2 <| tsub_le_tsub_left hp.1.out.le _

Premises used: Membership.mem.out, add_le_add, LT.lt.le, tsub_le_tsub_left, And.right, And.left, le_trans
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
⊢ p.1 < (↑r : ℝ≥0∞)

Tactic:
hp.1

Premises used: Set.Mem, setOf, And.left
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
⊢ p.1 < (↑r : ℝ≥0∞)

Tactic:
exact hp.1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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 ∈ closedEBall x R

Tactic:
calc
    edist z x ≤ edist z p.2 + edist p.2 x := edist_triangle _ _ _
    _ ≤ p.1 + (R - p.1) := add_le_add hz <| le_trans hp.2 <| tsub_le_tsub_left hp.1.out.le _
    _ = R := add_tsub_cancel_of_le (lt_trans (by exact hp.1) hrR).le

Premises used: Membership.mem.out, add_le_add, HSub.hSub, lt_trans, LT.lt.le, Prod.fst, tsub_le_tsub_left, And.left, EDist.edist, Prod.snd, add_tsub_cancel_of_le, le_trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
⊢ ∀ᶠ (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
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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}
⊢ ∃ (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⟩

Premises used: Filter.Eventually.exists_gt
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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}

Tactic:
⟨r, hr.mono fun y hy => ⟨hr0, ?_⟩⟩

Premises used: Filter.Eventually.mono, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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
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}
⊢ ∃ (r : ℝ),
    ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}

Tactic:
refine ⟨r, hr.mono fun y hy => ⟨hr0, ?_⟩⟩
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
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)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (i : ι) (j : y ∈ K i), Membership.mem (γ := Set ℝ≥0∞) {r : ℝ≥0∞ | closedEBall y r ⊆ U i} (ENNReal.ofReal r)
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i}

Tactic:
rwa [mem_preimage, mem_iInter₂]

Premises used: Set.mem_iInter₂, Set.mem_preimage