awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
refine_1 :
  ∀ (k : β),
    nndist.{u_4} (α := Y) (Pi.single (M := fun (a : β) ↦ Y) i a k : Y) (Pi.single (M := fun (j : β) ↦ Y) j b k : Y) ≤
      max (nndist a 0) (nndist b 0)
refine_2 :
  nndist a 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)
refine_3 :
  nndist b 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)
⊢ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b) =
    max (nndist a 0) (nndist b 0)

Tactic:
refine le_antisymm (nndist_pi_le_iff.2 fun k ↦ ?_) (max_le ?_ ?_)

Premises used: Iff.mpr, nndist_pi_le_iff, le_antisymm, max_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
refine_1 : nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist.{u_4} (α := Y) (Pi.single (M := fun (a : β) ↦ Y) i a k : Y) (Pi.single (M := fun (j : β) ↦ Y) j b k : Y) ≤
    max (nndist a 0) (nndist b 0)

Tactic:
simp only [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
pos : ∀ (hki : k = i), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
neg : ∀ (hki : ¬k = i), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hki : k = i
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
pos : ∀ (hkj : k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
neg : ∀ (hkj : ¬k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hkj : k = j
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
pos : ∀ (hkj : k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
neg : ∀ (hkj : ¬k = j), nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hkj : k = j
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

Premises used: nndist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

Premises used: nndist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

Premises used: nndist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

Premises used: nndist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist a 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)

Tactic:
simpa [h] using nndist_le_pi_nndist (Pi.single i a : β → Y) (Pi.single j b) i

Premises used: nndist_le_pi_nndist, Pi.single
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist b 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)

Tactic:
simpa [h, nndist_comm] using nndist_le_pi_nndist (Pi.single i a : β → Y) (Pi.single j b) j

Premises used: nndist_le_pi_nndist, nndist_comm, Pi.single
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ dist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b) =
    max (dist a 0) (dist b 0)

Tactic:
simp only [dist_nndist, nndist_single_single i j a b h, NNReal.coe_max]

Premises used: nndist_single_single, dist_nndist, NNReal.coe_max
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
x y z : ℝ
h : y ∈ uIcc x z
⊢ dist x y ≤ dist x z

Tactic:
simpa only [dist_comm x] using abs_sub_left_of_mem_uIcc h

Premises used: dist_comm, Set.abs_sub_left_of_mem_uIcc
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
x y z : ℝ
h : y ∈ uIcc x z
⊢ dist y z ≤ dist x z

Tactic:
simpa only [dist_comm _ z] using abs_sub_right_of_mem_uIcc h

Premises used: Set.abs_sub_right_of_mem_uIcc, dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
rwa rwa₁ rwa₂ rwa₃ : y ∈ uIcc x' y'
⊢ y ∈ uIcc y' x'

Tactic:
rwa [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
rwa rwa₁ rwa₂ rwa₃ : x ∈ uIcc x' y'
⊢ x ∈ uIcc y' x'

Tactic:
rwa [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
x y x' y' : ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ y' - x'

Tactic:
simpa only [Real.dist_eq, abs_of_nonpos (sub_nonpos.2 <| hx.1.trans hx.2), neg_sub] using
    Real.dist_le_of_mem_uIcc (Icc_subset_uIcc hx) (Icc_subset_uIcc hy)

Premises used: Iff.mpr, neg_sub, Set.Icc_subset_uIcc, Real.dist_le_of_mem_uIcc, abs_of_nonpos, And.right, Real.dist_eq, And.left, LE.le.trans, sub_nonpos
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) x
hy : Membership.mem (γ := Set ℝ) (Icc 0 1) y
⊢ dist x y ≤ 1

Tactic:
simpa only [sub_zero] using Real.dist_le_of_mem_Icc hx hy

Premises used: sub_zero, Real.dist_le_of_mem_Icc
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ dist x' y'

Tactic:
(dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b)

Premises used: Iff.mpr, dist_nonneg, dist_pi_le_iff, Real.dist_le_of_mem_uIcc, LE.le.trans, dist_le_pi_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
refine_1 : ∀ (b : ι), x b ∈ uIcc (x' b) (y' b)
refine_2 : ∀ (b : ι), y b ∈ uIcc (x' b) (y' b)
⊢ dist x y ≤ dist x' y'

Tactic:
refine (dist_pi_le_iff dist_nonneg).2 fun b =>
    (Real.dist_le_of_mem_uIcc ?_ ?_).trans (dist_le_pi_dist x' y' b)

Premises used: Iff.mpr, dist_nonneg, dist_pi_le_iff, Real.dist_le_of_mem_uIcc, LE.le.trans, dist_le_pi_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ uIcc (x' b) (y' b)

Tactic:
Icc_subset_uIcc ?_

Premises used: Set.Icc_subset_uIcc
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
refine_1 : x b ∈ Icc (x' b) (y' b)
⊢ x b ∈ uIcc (x' b) (y' b)

Tactic:
refine Icc_subset_uIcc ?_

Premises used: Set.Icc_subset_uIcc
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ uIcc (x' b) (y' b)

Tactic:
Icc_subset_uIcc ?_

Premises used: Set.Icc_subset_uIcc
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
refine_2 : y b ∈ Icc (x' b) (y' b)
⊢ y b ∈ uIcc (x' b) (y' b)

Tactic:
refine Icc_subset_uIcc ?_

Premises used: Set.Icc_subset_uIcc
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ Icc (x' b) (y' b)

Tactic:
⟨hx.1 _, hx.2 _⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ y b ∈ Icc (x' b) (y' b)

Tactic:
⟨hy.1 _, hy.2 _⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Real
Goal:
ι : Type u_1
inst : Fintype ι
x y x' y' : ι → ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
b : ι
⊢ x b ∈ Icc (x' b) (y' b)

Tactic:
exacts [⟨hx.1 _, hx.2 _⟩, ⟨hy.1 _, hy.2 _⟩]
-- Module: Mathlib.Topology.MetricSpace.Sequences
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : ProperSpace X
s : Set X
hs : Bornology.IsBounded s
x : ℕ → X
hx : ∃ᶠ (n : ℕ) in atTop, x n ∈ s
⊢ ∃ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s,
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
have hcs : IsSeqCompact (closure s) := hs.isCompact_closure.isSeqCompact
  have hu' : ∃ᶠ n in atTop, x n ∈ closure s := hx.mono fun _n hn => subset_closure hn
  hcs.subseq_of_frequently_in hu'

Premises used: subset_closure, IsSeqCompact.subseq_of_frequently_in, Bornology.IsBounded.isCompact_closure, Filter.Frequently.mono, IsCompact.isSeqCompact
-- Module: Mathlib.Topology.MetricSpace.Sequences
Goal:
X : Type u_1
inst : PseudoMetricSpace X
inst_1 : ProperSpace X
s : Set X
hs : Bornology.IsBounded s
x : ℕ → X
hx : ∀ (n : ℕ), x n ∈ s
⊢ ∃ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s,
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
tendsto_subseq_of_frequently_bounded hs <| Frequently.of_forall hx

Premises used: Filter.Frequently.of_forall, tendsto_subseq_of_frequently_bounded
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
rcases :
  ∀ (v : ι → Set α) (hsv : s ⊆ iUnion v)
    (hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i))
    (hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)), ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
    ⟨v, hsv, hvc, hcv⟩

Premises used: exists_subset_iUnion_closed_subset, Metric.isOpen_ball
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∀ (i : ι), ∃ r' < r i, v i ⊆ ball (c i) r'

Tactic:
have := fun i => exists_lt_subset_ball (hvc i) (hcv i)
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r' < r i, v i ⊆ ball (c i) r'
choose :
  ∀ (r' : (i : ι) → ℝ) (hlt : ∀ (i : ι), r' i < r i) (hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)),
    ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
choose r' hlt hsub using this
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : (i : ι) → ℝ
hlt : ∀ (i : ι), r' i < r i
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, Set.iUnion_mono
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : (i : ι) → ℝ
hlt : ∀ (i : ι), r' i < r i
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
exact ⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
r : ι → ℝ
uf : ∀ (x : α), Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
uU : Eq.{u + 1} (α := Set α) (⋃ (i : ι), ball (c i) (r i)) univ
⊢ ∃ (r' : ι → ℝ), Eq.{u + 1} (α := Set α) (⋃ (i : ι), ball (c i) (r' i)) univ ∧ ∀ (i : ι), r' i < r i

Tactic:
let ⟨r', hU, hv⟩ := exists_subset_iUnion_ball_radius_lt isClosed_univ (fun x _ => uf x) uU.ge
  ⟨r', univ_subset_iff.1 hU, hv⟩

Premises used: isClosed_univ, Set.univ_subset_iff, Eq.ge, Set.univ, Exists, Metric.ball, And, exists_subset_iUnion_ball_radius_lt, And.intro, Exists.intro, Iff.mp, _private.0.exists_iUnion_ball_eq_radius_lt.match_1, Eq, Set.iUnion
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
rcases :
  ∀ (v : ι → Set α) (hsv : s ⊆ iUnion v)
    (hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i))
    (hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)),
    ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
    ⟨v, hsv, hvc, hcv⟩

Premises used: exists_subset_iUnion_closed_subset, Metric.isOpen_ball
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'

Tactic:
have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'
choose :
  ∀ (r' : (i : ι) → ℝ) (hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)) (hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)),
    ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
choose r' hlt hsub using this
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : (i : ι) → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro, Set.iUnion_mono
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : (i : ι) → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ (r' : ι → ℝ), s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
ι : Type v
inst : MetricSpace α
inst_1 : ProperSpace α
c : ι → α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
uf : ∀ (x : α), Set.Finite.{v} (α := ι) {i : ι | x ∈ ball (c i) (r i)}
uU : Eq.{u + 1} (α := Set α) (⋃ (i : ι), ball (c i) (r i)) univ
⊢ ∃ (r' : ι → ℝ), Eq.{u + 1} (α := Set α) (⋃ (i : ι), ball (c i) (r' i)) univ ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
let ⟨r', hU, hv⟩ :=
    exists_subset_iUnion_ball_radius_pos_lt hr isClosed_univ (fun x _ => uf x) uU.ge
  ⟨r', univ_subset_iff.1 hU, hv⟩

Premises used: isClosed_univ, Set.univ_subset_iff, Eq.ge, Set.univ, Exists, Metric.ball, exists_subset_iUnion_ball_radius_pos_lt, And, And.intro, Exists.intro, Iff.mp, _private.0.exists_iUnion_ball_eq_radius_pos_lt.match_1, Eq, Set.iUnion
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
⊢ ∀ x ∈ s, (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R x) fun (r : ℝ) ↦ ball x r

Tactic:
have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
    nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R x) fun (r : ℝ) ↦ ball x r
rcases :
  ∀ (ι : Type u) (c : ι → α) (r' : (a : ι) → ℝ) (hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a))
    (hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)) (hfin : LocallyFinite (X := α) fun (a : ι) ↦ ball (c a) (r' a)),
    ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
      (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
        (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)

Tactic:
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with
    ⟨ι, c, r', hr', hsub', hfin⟩

Premises used: refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set
-- Module: Mathlib.Topology.MetricSpace.ShrinkingLemma
Goal:
α : Type u
inst : MetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R x) fun (r : ℝ) ↦ ball x r
ι : Type u
c : ι → α
r' : (a : ι) → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)
hfin : LocallyFinite (X := α) fun (a : ι) ↦ ball (c a) (r' a)
rcases :
  ∀ (r : ι → ℝ) (hsub : s ⊆ ⋃ (i : ι), ball (c i) (r i)) (hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)),
    ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
      (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
        (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ (ι : Type u) (c : ι → α) (r : ι → ℝ) (r' : ι → ℝ),
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite (X := α) fun (i : ι) ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)

Tactic:
rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs
      (fun x _ => hfin.point_finite x) hsub' with
    ⟨r, hsub, hlt⟩

Premises used: exists_subset_iUnion_ball_radius_pos_lt, And.right, And.left, LocallyFinite.point_finite