awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
inl :
  ∀ (H₁ : a.r i ≤ dist (a.c i) (a.c j)) (H₂ : a.r j ≤ τ * a.r i),
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
        (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
        (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
inr :
  ∀ (H₁ : a.r j ≤ dist (a.c j) (a.c i)) (H₂ : a.r i ≤ τ * a.r j),
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
        (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
        (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩)

Premises used: Besicovitch.SatelliteConfig.h
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
inl :
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
left
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
inr :
  (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
right
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
inl :
  ∀ (H₁ : a.r i ≤ dist (a.c i) (a.c j)) (H₂ : a.r j ≤ τ * a.r i),
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
inr :
  ∀ (H₁ : a.r j ≤ dist (a.c j) (a.c i)) (H₂ : a.r i ≤ τ * a.r j),
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩) <;> [left; right]

Premises used: Besicovitch.SatelliteConfig.h
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
inl : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)
inl₁ : (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
inr : (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)
inr₁ : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
inl : 0 ≤ (a.r (last N))⁻¹
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
inl : 0 ≤ (a.r (last N))⁻¹
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
inr : 0 ≤ (a.r (last N))⁻¹
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
inr : 0 ≤ (a.r (last N))⁻¹
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
simp :
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
⊢ (a.r (last N))⁻¹ * a.r i ≤
      dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c (last N) - a.c (last N))) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ τ * ((a.r (last N))⁻¹ * a.r i)

Tactic:
simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
      Real.norm_of_nonneg]

Premises used: dist_sub_right, mul_left_comm, dist_smul₀, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
⊢ a.r i ≤ dist (a.c i) (a.c (last N))

Tactic:
have ⟨H₁, H₂⟩ := a.hlast i hi
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
⊢ a.r (last N) ≤ τ * a.r i

Tactic:
have ⟨H₁, H₂⟩ := a.hlast i hi
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
left : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))
right : (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
left : 0 ≤ (a.r (last N))⁻¹
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
right : 0 ≤ (a.r (last N))⁻¹
⊢ (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
simp : (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ≤ (a.r (last N))⁻¹ * (a.r i + a.r (last N))
⊢ dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c (last N) - a.c (last N))) ≤
    (a.r (last N))⁻¹ * a.r i + (a.r (last N))⁻¹ * a.r (last N)

Tactic:
simp (disch := positivity) only [dist_smul₀, ← mul_add, dist_sub_right, Real.norm_of_nonneg]

Premises used: dist_sub_right, dist_smul₀, mul_add, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
hbc : dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
⊢ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ≤ (a.r (last N))⁻¹ * (a.r i + a.r (last N))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
a.inter i hi

Premises used: Besicovitch.SatelliteConfig.inter
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
exact a.inter i hi

Premises used: Besicovitch.SatelliteConfig.inter
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
⊢ a.centerAndRescale.c (last N) = 0

Tactic:
simp [SatelliteConfig.centerAndRescale]

Premises used: Besicovitch.SatelliteConfig.centerAndRescale
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
⊢ a.centerAndRescale.r (last N) = 1

Tactic:
simp [SatelliteConfig.centerAndRescale, inv_mul_cancel₀ (a.rpos _).ne']

Premises used: Besicovitch.SatelliteConfig.centerAndRescale, Besicovitch.SatelliteConfig.rpos, LT.lt.ne', inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
⊢ 0 < ρ

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
⊢ 0 < ρ

Tactic:
have ρpos : 0 < ρ := by norm_num
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
⊢ let A : Set E := ⋃ c ∈ s, ball c δ;
  A = ⋃ c ∈ s, ball c δ

Tactic:
set A := ⋃ c ∈ s, ball (c : E) δ with hA
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
h₁ : δ + δ ≤ dist c d
⊢ Function.onFun (β := Set E) Disjoint (fun (c : E) ↦ ball c δ) c d

Tactic:
apply ball_disjoint_ball

Premises used: Metric.ball_disjoint_ball
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
h₁ : δ + δ ≤ ‖c - d‖
⊢ δ + δ ≤ dist c d

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
⊢ 1 ≤ ‖c - d‖

Tactic:
h c hc d hd hcd
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
h₁ : δ + δ = 1
⊢ δ + δ ≤ ‖c - d‖

Tactic:
convert! h c hc d hd hcd
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
⊢ δ + δ = 1

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
⊢ (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)

Tactic:
have D : Set.Pairwise (s : Set E) (Disjoint on fun c => ball (c : E) δ) := by
    rintro c hc d hd hcd
    apply ball_disjoint_ball
    rw [dist_eq_norm]
    convert! h c hc d hd hcd
    norm_num
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
⊢ A ⊆ ball 0 ρ

Tactic:
iUnion₂_subset fun x hx => ?_

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
refine : ∀ (x : E) (hx : x ∈ s), ball x δ ⊆ ball 0 ρ
⊢ A ⊆ ball 0 ρ

Tactic:
refine iUnion₂_subset fun x hx => ?_

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
x : E
hx : x ∈ s
h₁ : δ + dist x 0 ≤ ρ
⊢ ball x δ ⊆ ball 0 ρ

Tactic:
apply ball_subset_ball'

Premises used: Metric.ball_subset_ball'
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
x : E
hx : x ∈ s
rw : δ + ‖x‖ ≤ δ + 2
⊢ δ + dist x 0 ≤ δ + 2

Tactic:
rw [dist_zero_right]

Premises used: dist_zero_right
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
x : E
hx : x ∈ s
⊢ δ + ‖x‖ ≤ δ + 2

Tactic:
add_le_add le_rfl (hs x hx)

Premises used: le_rfl, add_le_add
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
x : E
hx : x ∈ s
⊢ δ + ‖x‖ ≤ δ + 2

Tactic:
exact add_le_add le_rfl (hs x hx)

Premises used: le_rfl, add_le_add
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
x : E
hx : x ∈ s
⊢ δ + 2 = 5 / 2

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
x : E
hx : x ∈ s
δ₁ : δ + dist x 0 ≤ δ + 2
δ₂ : δ + 2 = 5 / 2
⊢ δ + dist x 0 ≤ ρ

Tactic:
calc
      δ + dist x 0 ≤ δ + 2 := by rw [dist_zero_right]; exact add_le_add le_rfl (hs x hx)
      _ = 5 / 2 := by norm_num

Premises used: Dist.dist, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
⊢ A ⊆ ball 0 ρ

Tactic:
have A_subset : A ⊆ ball (0 : E) ρ := by
    refine iUnion₂_subset fun x hx => ?_
    apply ball_subset_ball'
    calc
      δ + dist x 0 ≤ δ + 2 := by rw [dist_zero_right]; exact add_le_add le_rfl (hs x hx)
      _ = 5 / 2 := by norm_num
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
A_subset : A ⊆ ball 0 ρ
rw :
  HMul.hMul (β := ℝ≥0∞) ((↑s.card : ℝ≥0∞) * ENNReal.ofReal (δ ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
    ∑ p ∈ s, (μ : (a : Set E) → ℝ≥0∞) (ball p δ)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑s.card : ℝ≥0∞) * ENNReal.ofReal (δ ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
    (μ : (a : Set E) → ℝ≥0∞) A

Tactic:
rw [hA, measure_biUnion_finset D fun c _ => measurableSet_ball]

Premises used: measurableSet_ball, MeasureTheory.measure_biUnion_finset
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ 0 < δ

Tactic:
norm_num