awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
have obtain : ∀ (g : E → F) (h'g : EqOn f g (insert x s)) (hg : AnalyticAt 𝕜 g x), ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
Tactic: obtain ⟨g, -, h'g, hg⟩ : ∃ g, f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x :=
    h.exists_analyticAt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
have refine_1 : u ∈ 𝓝[insert x s] x
Tactic: refine ⟨u, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
refine_1 : u ∈ 𝓝[insert x s] x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
have refine_2 : AnalyticOn 𝕜 f u
Tactic: refine ⟨u, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
h : AnalyticWithinAt 𝕜 f s x
g : E → F
h'g : EqOn f g (insert x s)
hg : AnalyticAt 𝕜 g x
u : Set E := insert x s ∩ {y : E | AnalyticAt 𝕜 g y}
y : E
hy : y ∈ u
⊢ AnalyticWithinAt 𝕜 f u y
have this : AnalyticWithinAt 𝕜 g u y
Tactic: have : AnalyticWithinAt 𝕜 g u y := hy.2.analyticWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
⊢ ∀ᶠ (y : E) in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y
have obtain : ∀ (g : E → F) (hfg : f =ᶠ[𝓝[insert x s] x] g) (hga : AnalyticAt 𝕜 g x), ∀ᶠ (y : E) in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y
Tactic: obtain ⟨g, hfg, hga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hfg : f =ᶠ[𝓝[insert x s] x] g
hga : AnalyticAt 𝕜 g x
⊢ ∀ᶠ (y : E) in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y
have simp : ∀ (hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1), ∀ᶠ (x : E) in 𝓝 x, x ∈ s → AnalyticWithinAt 𝕜 f s x
Tactic: simp only [Filter.EventuallyEq, eventually_nhdsWithin_iff] at hfg ⊢
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
⊢ ∀ᶠ (x : E) in 𝓝 x, x ∈ s → AnalyticWithinAt 𝕜 f s x
have h : ∀ (z : E) (hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1) (hgaz : AnalyticAt 𝕜 g z) (hz : z ∈ s),
  AnalyticWithinAt 𝕜 f s z
Tactic: filter_upwards [hfg.eventually_nhds, hga.eventually_analyticAt] with z hfgz hgaz hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Within (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
g : E → F
hga : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ insert x s → f x_1 = g x_1
z : E
hfgz : ∀ᶠ (x_1 : E) in 𝓝 z, x_1 ∈ insert x s → f x_1 = g x_1
hgaz : AnalyticAt 𝕜 g z
hz : z ∈ s
⊢ AnalyticWithinAt 𝕜 f s z
have h : f =ᶠ[𝓝[insert z s] z] g
Tactic: refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨g, ?_, hgaz⟩
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (hypothesis)
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
⊢ (↑D.packingRadius : ℝ) < dist x y
have hsep : ENNReal.ofReal (↑D.packingRadius : ℝ) < ENNReal.ofReal (dist x y)
Tactic: have hsep : ENNReal.ofReal D.packingRadius < ENNReal.ofReal (dist x y) := by
    simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
Goal:
X : Type u_1
inst : MetricSpace X
D : DeloneSet X
x : X
⊢ ∃ y ∈ D, dist x y ≤ (↑D.coveringRadius : ℝ)
have 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 : ℝ)
Tactic: obtain ⟨y, hy, hdist⟩ := D.isCover_coveringRadius (x := x) (by trivial)
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
⊢ x = y
have by_contra : ∀ (hne : ¬x = y), False
Tactic: by_contra hne
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 + dist y z < (↑r : ℝ) + (↑r : ℝ)
have h₁ : dist x z < (↑r : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
⊢ dist x z + dist y z < (↑r : ℝ) + (↑r : ℝ)
have h₂ : dist y z < (↑r : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
have rw : (↑r : ℝ) + (↑r : ℝ) ≤ (↑(D.packingRadius / 2) : ℝ) + (↑(D.packingRadius / 2) : ℝ)
Tactic: rw [← add_halves D.packingRadius, NNReal.coe_add]
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 = D
have carrier : ∀ (x : X), x ∈ (mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).carrier ↔ x ∈ D.carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D
have packingRadius : (↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).packingRadius : ℝ) = (↑D.packingRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D
have coveringRadius : (↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).coveringRadius : ℝ) = (↑D.coveringRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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) =
    mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D
have 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) sorry sorry sorry sorry D).carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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
⊢ 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
have 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) sorry sorry sorry sorry D).packingRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
⊢ 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
have 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) sorry sorry sorry sorry D).coveringRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 ∈
      (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
have 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
Tactic: simp only [mapBilipschitz_carrier, Equiv.trans_apply, Set.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet 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
have carrier : ∀ (x : X),
  Membership.mem (γ := Set X)
      (carrier
        ((fun (D : DeloneSet Y) ↦
            (mapBilipschitz f.symm.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
              D.coveringRadius sorry sorry sorry)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius sorry sorry sorry)
            D)))
      x ↔
    x ∈ D.carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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
⊢ (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
have packingRadius : (↑(packingRadius.{u_1} (X := X)
        ((fun (D : DeloneSet Y) ↦
            (mapBilipschitz f.symm.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
              D.coveringRadius sorry sorry sorry)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius sorry sorry sorry)
            D))) :
    ℝ) =
  (↑D.packingRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
⊢ (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
have coveringRadius : (↑(coveringRadius.{u_1} (X := X)
        ((fun (D : DeloneSet Y) ↦
            (mapBilipschitz f.symm.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
              D.coveringRadius sorry sorry sorry)
          ((fun (D : DeloneSet X) ↦
              (mapBilipschitz f.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
                D.coveringRadius sorry sorry sorry)
            D))) :
    ℝ) =
  (↑D.coveringRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : MetricSpace X
inst_1 : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet 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
have carrier : ∀ (x : Y),
  Membership.mem (γ := Set Y)
      (carrier
        ((fun (D : DeloneSet X) ↦
            (mapBilipschitz f.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
              D.coveringRadius sorry sorry sorry)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius sorry sorry sorry)
            D)))
      x ↔
    x ∈ D.carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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
⊢ (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
have packingRadius : (↑(packingRadius.{u_2} (X := Y)
        ((fun (D : DeloneSet X) ↦
            (mapBilipschitz f.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
              D.coveringRadius sorry sorry sorry)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius sorry sorry sorry)
            D))) :
    ℝ) =
  (↑D.packingRadius : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.AperiodicOrder.Delone.Basic (goal)
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 : ℝ)
⊢ (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
have coveringRadius : (↑(coveringRadius.{u_2} (X := Y)
        ((fun (D : DeloneSet X) ↦
            (mapBilipschitz f.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f : (a : X) → Y) '' D.carrier) D.packingRadius
              D.coveringRadius sorry sorry sorry)
          ((fun (D : DeloneSet Y) ↦
              (mapBilipschitz f.symm.toEquiv 1 1 sorry sorry sorry sorry D).copy ((⇑f.symm : (a : Y) → X) '' D.carrier) D.packingRadius
                D.coveringRadius sorry sorry sorry)
            D))) :
    ℝ) =
  (↑D.coveringRadius : ℝ)
Tactic: ext