awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x : X
⊢ Membership.mem (γ := Set X) Set.univ x

Tactic:
trivial
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x : X
obtain :
  ∀ (y : X) (hy : y ∈ D.carrier)
    (hdist :
      Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑D.coveringRadius : ENNReal)}
        (x, y)),
    ∃ y ∈ D, dist x y ≤ (↑D.coveringRadius : ℝ)
⊢ ∃ y ∈ D, dist x y ≤ (↑D.coveringRadius : ℝ)

Tactic:
obtain ⟨y, hy, hdist⟩ := D.isCover_coveringRadius (x := x) (by trivial)

Premises used: Delone.DeloneSet.isCover_coveringRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hy : y ∈ D.carrier
hdist :
  Membership.mem (γ := SetRel X X)
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => edist x y ≤ (↑D.coveringRadius : ENNReal)}
    (x, y)
⊢ dist x y ≤ (↑D.coveringRadius : ℝ)

Tactic:
simpa [edist_dist] using hdist

Premises used: edist_dist
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hy : y ∈ D.carrier
hdist :
  Membership.mem (γ := SetRel X X)
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => edist x y ≤ (↑D.coveringRadius : ENNReal)}
    (x, y)
⊢ ∃ y ∈ D, dist x y ≤ (↑D.coveringRadius : ℝ)

Tactic:
exact ⟨y, hy, by simpa [edist_dist] using hdist⟩
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
by_contra : ∀ (hne : ¬x = y), False
⊢ x = y

Tactic:
by_contra hne
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
hne : ¬x = y
h₁ : dist x z < (↑r : ℝ)
h₂ : dist y z < (↑r : ℝ)
⊢ dist x z + dist y z < (↑r : ℝ) + (↑r : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
hne : ¬x = y
⊢ dist x z < (↑r : ℝ)

Tactic:
simpa
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
hne : ¬x = y
⊢ dist y z < (↑r : ℝ)

Tactic:
simpa
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
hne : ¬x = y
rw : (↑r : ℝ) + (↑r : ℝ) ≤ (↑(D.packingRadius / 2) : ℝ) + (↑(D.packingRadius / 2) : ℝ)
⊢ (↑r : ℝ) + (↑r : ℝ) ≤ (↑D.packingRadius : ℝ)

Tactic:
rw [← add_halves D.packingRadius, NNReal.coe_add]

Premises used: NNReal.coe_add, add_halves, Delone.DeloneSet.packingRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
hne : ¬x = y
⊢ (↑r : ℝ) + (↑r : ℝ) ≤ (↑(D.packingRadius / 2) : ℝ) + (↑(D.packingRadius / 2) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z (↑r : ℝ)
hyz : y ∈ ball z (↑r : ℝ)
hne : ¬x = y
⊢ False

Tactic:
exact (D.packingRadius_lt_dist_of_mem_ne hx hy hne).not_gt <| calc
    dist x y ≤ dist x z + dist y z := dist_triangle_right x y z
    _ < r + r := by gcongr <;> simpa
    _ ≤ D.packingRadius := by rw [← add_halves D.packingRadius, NNReal.coe_add]; gcongr

Premises used: dist_triangle_right, Delone.DeloneSet.packingRadius_lt_dist_of_mem_ne, LT.lt.not_gt, Dist.dist, Delone.DeloneSet.packingRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
⊢ ∃ r > 0, ∀ {x y z : X}, x ∈ D → y ∈ D → x ∈ ball z r → y ∈ ball z r → x = y

Tactic:
⟨D.packingRadius / 2, half_pos D.packingRadius_pos, fun hx hy => D.eq_of_mem_ball le_rfl hx hy⟩

Premises used: le_rfl, half_pos, HDiv.hDiv, Delone.DeloneSet.packingRadius_pos, And.intro, Exists.intro, Delone.DeloneSet.eq_of_mem_ball, OfNat.ofNat, NNReal.toReal, Delone.DeloneSet.packingRadius
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
hK1 hK2 : LT.lt (α := ℝ≥0) 0 1
hA : AntilipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
hL : LipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
carrier : ∀ (x : X), x ∈ (mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).carrier ↔ x ∈ D.carrier
packingRadius : (↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).packingRadius : ℝ) = (↑D.packingRadius : ℝ)
coveringRadius : (↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).coveringRadius : ℝ) = (↑D.coveringRadius : ℝ)
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D

Tactic:
ext
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
hK1 hK2 : LT.lt (α := ℝ≥0) 0 1
hA : AntilipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
hL : LipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
x : X
⊢ x ∈ (mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).carrier ↔ x ∈ D.carrier

Tactic:
simp only [mapBilipschitz, Equiv.refl_apply, Set.image_id', div_one, one_mul]

Premises used: Equiv.refl_apply, Delone.DeloneSet.mapBilipschitz, Set.image_id', div_one, one_mul
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
hK1 hK2 : LT.lt (α := ℝ≥0) 0 1
hA : AntilipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
hL : LipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
⊢ (↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).packingRadius : ℝ) = (↑D.packingRadius : ℝ)

Tactic:
simp only [mapBilipschitz, Equiv.refl_apply, Set.image_id', div_one, one_mul]

Premises used: Equiv.refl_apply, Delone.DeloneSet.mapBilipschitz, Set.image_id', div_one, one_mul
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
hK1 hK2 : LT.lt (α := ℝ≥0) 0 1
hA : AntilipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
hL : LipschitzWith (α := X) (β := X) 1 (⇑(Equiv.refl X) : (a : X) → X)
⊢ (↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).coveringRadius : ℝ) = (↑D.coveringRadius : ℝ)

Tactic:
simp only [mapBilipschitz, Equiv.refl_apply, Set.image_id', div_one, one_mul]

Premises used: Equiv.refl_apply, Delone.DeloneSet.mapBilipschitz, Set.image_id', div_one, one_mul
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith.{u_1, u_2} (α := X) (β := Y) K₁f (⇑f : (a : X) → Y)
hf_lip : LipschitzWith.{u_1, u_2} (α := X) (β := Y) K₂f (⇑f : (a : X) → Y)
hg_anti : AntilipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₁g (⇑g : (a : Y) → Z)
hg_lip : LipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₂g (⇑g : (a : Y) → Z)
carrier :
  ∀ (x : Z),
    x ∈
        (mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
            (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).carrier ↔
      x ∈ (mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).carrier
packingRadius :
  (↑(mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
            (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).packingRadius :
      ℝ) =
    (↑(mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).packingRadius : ℝ)
coveringRadius :
  (↑(mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
            (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).coveringRadius :
      ℝ) =
    (↑(mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).coveringRadius : ℝ)
⊢ mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) =
    mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D

Tactic:
ext
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith.{u_1, u_2} (α := X) (β := Y) K₁f (⇑f : (a : X) → Y)
hf_lip : LipschitzWith.{u_1, u_2} (α := X) (β := Y) K₂f (⇑f : (a : X) → Y)
hg_anti : AntilipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₁g (⇑g : (a : Y) → Z)
hg_lip : LipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₂g (⇑g : (a : Y) → Z)
x : Z
carrier :
  (∃ (x_1 : Y), (∃ x ∈ D.carrier, (f : (a : X) → Y) x = x_1) ∧ (g : (a : Y) → Z) x_1 = x) ↔
    ∃ x_1 ∈ D.carrier, (g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) = x
⊢ x ∈
      (mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
          (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).carrier ↔
    x ∈ (mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).carrier

Tactic:
simp only [mapBilipschitz_carrier, Equiv.trans_apply, Set.mem_image]

Premises used: Equiv.trans_apply, Set.mem_image, Delone.DeloneSet.mapBilipschitz_carrier
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith.{u_1, u_2} (α := X) (β := Y) K₁f (⇑f : (a : X) → Y)
hf_lip : LipschitzWith.{u_1, u_2} (α := X) (β := Y) K₂f (⇑f : (a : X) → Y)
hg_anti : AntilipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₁g (⇑g : (a : Y) → Z)
hg_lip : LipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₂g (⇑g : (a : Y) → Z)
x : Z
⊢ (∃ (x_1 : Y), (∃ x ∈ D.carrier, (f : (a : X) → Y) x = x_1) ∧ (g : (a : Y) → Z) x_1 = x) ↔
    ∃ x_1 ∈ D.carrier, (g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) = x

Tactic:
exists_exists_and_eq_and

Premises used: exists_exists_and_eq_and
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith.{u_1, u_2} (α := X) (β := Y) K₁f (⇑f : (a : X) → Y)
hf_lip : LipschitzWith.{u_1, u_2} (α := X) (β := Y) K₂f (⇑f : (a : X) → Y)
hg_anti : AntilipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₁g (⇑g : (a : Y) → Z)
hg_lip : LipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₂g (⇑g : (a : Y) → Z)
x : Z
⊢ (∃ (x_1 : Y), (∃ x ∈ D.carrier, (f : (a : X) → Y) x = x_1) ∧ (g : (a : Y) → Z) x_1 = x) ↔
    ∃ x_1 ∈ D.carrier, (g : (a : Y) → Z) ((f : (a : X) → Y) x_1 : Y) = x

Tactic:
exact exists_exists_and_eq_and

Premises used: exists_exists_and_eq_and
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith.{u_1, u_2} (α := X) (β := Y) K₁f (⇑f : (a : X) → Y)
hf_lip : LipschitzWith.{u_1, u_2} (α := X) (β := Y) K₂f (⇑f : (a : X) → Y)
hg_anti : AntilipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₁g (⇑g : (a : Y) → Z)
hg_lip : LipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₂g (⇑g : (a : Y) → Z)
⊢ (↑(mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
            (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).packingRadius :
      ℝ) =
    (↑(mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).packingRadius : ℝ)

Tactic:
simp only [mapBilipschitz_packingRadius, NNReal.coe_div, div_div]

Premises used: NNReal.coe_div, Delone.DeloneSet.mapBilipschitz_packingRadius, div_div
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
Z : Type u_3
inst_2 : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith.{u_1, u_2} (α := X) (β := Y) K₁f (⇑f : (a : X) → Y)
hf_lip : LipschitzWith.{u_1, u_2} (α := X) (β := Y) K₂f (⇑f : (a : X) → Y)
hg_anti : AntilipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₁g (⇑g : (a : Y) → Z)
hg_lip : LipschitzWith.{u_2, u_3} (α := Y) (β := Z) K₂g (⇑g : (a : Y) → Z)
⊢ (↑(mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
            (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).coveringRadius :
      ℝ) =
    (↑(mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).coveringRadius : ℝ)

Tactic:
simp only [mapBilipschitz_coveringRadius, NNReal.coe_mul, mul_assoc]

Premises used: Delone.DeloneSet.mapBilipschitz_coveringRadius, mul_assoc, NNReal.coe_mul
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ D.packingRadius = (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).packingRadius

Tactic:
simp [mapBilipschitz]

Premises used: Delone.DeloneSet.mapBilipschitz
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ D.coveringRadius = (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).coveringRadius

Tactic:
simp [mapBilipschitz]

Premises used: Delone.DeloneSet.mapBilipschitz
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ D.packingRadius = (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).packingRadius

Tactic:
simp [mapBilipschitz]

Premises used: Delone.DeloneSet.mapBilipschitz
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ D.coveringRadius = (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).coveringRadius

Tactic:
simp [mapBilipschitz]

Premises used: Delone.DeloneSet.mapBilipschitz
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
carrier :
  ∀ (x : X),
    Membership.mem (γ := Set X)
        (DeloneSet.carrier
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet X) ↦
                (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                  D.coveringRadius ⋯ ⋯ ⋯)
              D)))
        x ↔
      x ∈ D.carrier
packingRadius :
  (↑(DeloneSet.packingRadius.{u_1} (X := X)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet X) ↦
                (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                  D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.packingRadius : ℝ)
coveringRadius :
  (↑(DeloneSet.coveringRadius.{u_1} (X := X)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet X) ↦
                (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                  D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.coveringRadius : ℝ)
⊢ (fun (D : DeloneSet Y) ↦
        (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
          D.coveringRadius ⋯ ⋯ ⋯)
      ((fun (D : DeloneSet X) ↦
          (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
            D.coveringRadius ⋯ ⋯ ⋯)
        D) =
    D

Tactic:
ext
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
x : X
⊢ Membership.mem (γ := Set X)
      (carrier
        ((fun (D : DeloneSet Y) ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
              D.coveringRadius ⋯ ⋯ ⋯)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            D)))
      x ↔
    x ∈ D.carrier

Tactic:
simp [copy_eq]

Premises used: Delone.DeloneSet.copy_eq
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ (↑(packingRadius.{u_1} (X := X)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet X) ↦
                (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                  D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.packingRadius : ℝ)

Tactic:
simp [copy_eq]

Premises used: Delone.DeloneSet.copy_eq
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ (↑(coveringRadius.{u_1} (X := X)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet X) ↦
                (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                  D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.coveringRadius : ℝ)

Tactic:
simp [copy_eq]

Premises used: Delone.DeloneSet.copy_eq
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
carrier :
  ∀ (x : Y),
    Membership.mem (γ := Set Y)
        (DeloneSet.carrier
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet Y) ↦
                (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier)
                  D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
              D)))
        x ↔
      x ∈ D.carrier
packingRadius :
  (↑(DeloneSet.packingRadius.{u_2} (X := Y)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet Y) ↦
                (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier)
                  D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.packingRadius : ℝ)
coveringRadius :
  (↑(DeloneSet.coveringRadius.{u_2} (X := Y)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet Y) ↦
                (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier)
                  D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.coveringRadius : ℝ)
⊢ (fun (D : DeloneSet X) ↦
        (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius D.coveringRadius
          ⋯ ⋯ ⋯)
      ((fun (D : DeloneSet Y) ↦
          (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
            D.coveringRadius ⋯ ⋯ ⋯)
        D) =
    D

Tactic:
ext
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
x : Y
⊢ Membership.mem (γ := Set Y)
      (carrier
        ((fun (D : DeloneSet X) ↦
            (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
              D.coveringRadius ⋯ ⋯ ⋯)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            D)))
      x ↔
    x ∈ D.carrier

Tactic:
simp [copy_eq]

Premises used: Delone.DeloneSet.copy_eq
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ (↑(packingRadius.{u_2} (X := Y)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet Y) ↦
                (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier)
                  D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.packingRadius : ℝ)

Tactic:
simp [copy_eq]

Premises used: Delone.DeloneSet.copy_eq
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ (↑(coveringRadius.{u_2} (X := Y)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius ⋯ ⋯ ⋯)
            ((fun (D : DeloneSet Y) ↦
                (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier)
                  D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
              D))) :
      ℝ) =
    (↑D.coveringRadius : ℝ)

Tactic:
simp [copy_eq]

Premises used: Delone.DeloneSet.copy_eq
-- Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
carrier :
  ∀ (x : X),
    Membership.mem (γ := Set X)
        (DeloneSet.carrier ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) x ↔
      x ∈ D.carrier
packingRadius :
  (↑(DeloneSet.packingRadius.{u_1} (X := X)
          ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) :
      ℝ) =
    (↑D.packingRadius : ℝ)
coveringRadius :
  (↑(DeloneSet.coveringRadius.{u_1} (X := X)
          ((mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D)) :
      ℝ) =
    (↑D.coveringRadius : ℝ)
⊢ (mapIsometry (IsometryEquiv.refl X) : (a : DeloneSet X) → DeloneSet X) D = D

Tactic:
ext