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 τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah :
  Pairwise fun (i j : Fin N.succ) ↦
    a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
d : E := (s / ‖a.c j‖) • a.c j
hd : d = (s / ‖a.c j‖) • a.c j
I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖
J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ
invs_nonneg : 0 ≤ 2 / s
⊢ 2 / s * (s / ‖a.c j‖) = 2 / ‖a.c j‖

Tactic:
field
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
ah :
  Pairwise fun (i j : Fin N.succ) ↦
    a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
hj : 2 < ‖a.c j‖
s : ℝ := ‖a.c i‖
hi : 2 < s
hij : s ≤ ‖a.c j‖
A : a.r i ≤ s
spos : 0 < s
d : E := (s / ‖a.c j‖) • a.c j
hd : d = (s / ‖a.c j‖) • a.c j
I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖
J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ
invs_nonneg : 0 ≤ 2 / s
δ₁ : 1 - δ = 2 / s * (s / 2 - s / 2 * δ)
δ₂ : 2 / s * (s / 2 - s / 2 * δ) ≤ 2 / s * ‖d - a.c i‖
δ₃ : 2 / s * ‖d - a.c i‖ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
calc
    1 - δ = 2 / s * (s / 2 - s / 2 * δ) := by field
    _ ≤ 2 / s * ‖d - a.c i‖ := by
      gcongr; linarith only [hcrj, I, J, hi]
    _ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖ := by
      conv_lhs => rw [norm_sub_rev, ← abs_of_nonneg invs_nonneg]
      rw [← Real.norm_eq_abs, ← norm_smul, smul_sub, hd, smul_smul]
      congr 3
      field

Premises used: Norm.norm, HMul.hMul, Besicovitch.SatelliteConfig.c, HSub.hSub, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
simp : ‖if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i‖ ≤ 2
⊢ ‖c' i‖ ≤ 2

Tactic:
simp only [c']
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
pos : ∀ (h : ‖a.c i‖ ≤ 2), ‖a.c i‖ ≤ 2
neg : ∀ (h : ¬‖a.c i‖ ≤ 2), ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
⊢ ‖if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i‖ ≤ 2

Tactic:
split_ifs with 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 τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ‖a.c i‖ ≤ 2
⊢ ‖a.c i‖ ≤ 2

Tactic:
h
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ‖a.c i‖ ≤ 2
⊢ ‖a.c i‖ ≤ 2

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ¬‖a.c i‖ ≤ 2
pos : ∀ (hi : ‖a.c i‖ = 0), ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
neg : ∀ (hi : ¬‖a.c i‖ = 0), ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
⊢ ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2

Tactic:
by_cases hi : ‖a.c i‖ = 0

Premises used: Besicovitch.SatelliteConfig.c
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ¬‖a.c i‖ ≤ 2
hi : ‖a.c i‖ = 0
⊢ ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2

Tactic:
simp [norm_smul, hi]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
i : Fin N.succ
h : ¬‖a.c i‖ ≤ 2
hi : ¬‖a.c i‖ = 0
⊢ ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2

Tactic:
simp [norm_smul, hi]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
⊢ ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2

Tactic:
have norm_c'_le : ∀ i, ‖c' i‖ ≤ 2 := by
    intro i
    simp only [c']
    split_ifs with h; · exact h
    by_cases hi : ‖a.c i‖ = 0 <;> simp [norm_smul, hi]
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
⊢ ∃ (c' : Fin N.succ → E), (∀ (n : Fin N.succ), ‖c' n‖ ≤ 2) ∧ Pairwise fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
⟨c', fun n => norm_c'_le n, fun i j inej => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
refine : ∀ (i j : Fin N.succ) (inej : i ≠ j), (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
⊢ ∃ (c' : Fin N.succ → E), (∀ (n : Fin N.succ), ‖c' n‖ ≤ 2) ∧ Pairwise fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
refine ⟨c', fun n => norm_c'_le n, fun i j inej => ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
inr :
  ∀
    (this :
      ∀ (i j : Fin N.succ) (inej : i ≠ j) (hij : ‖a.c i‖ ≤ ‖a.c j‖),
        (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j)
    (hij : ¬‖a.c i‖ ≤ ‖a.c j‖), 1 - δ ≤ ‖c' i - c' j‖
wlog : ∀ (i j : Fin N.succ) (inej : i ≠ j) (hij : ‖a.c i‖ ≤ ‖a.c j‖), 1 - δ ≤ ‖c' i - c' j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
wlog hij : ‖a.c i‖ ≤ ‖a.c j‖ generalizing i j

Premises used: Besicovitch.SatelliteConfig.c
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
this :
  ∀ (i j : Fin N.succ) (inej : i ≠ j) (hij : ‖a.c i‖ ≤ ‖a.c j‖), (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
hij : ¬‖a.c i‖ ≤ ‖a.c j‖
inr : 1 - δ ≤ ‖c' j - c' i‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
rw [norm_sub_rev]

Premises used: norm_sub_rev
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
this :
  ∀ (i j : Fin N.succ) (inej : i ≠ j) (hij : ‖a.c i‖ ≤ ‖a.c j‖), (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
hij : ¬‖a.c i‖ ≤ ‖a.c j‖
⊢ 1 - δ ≤ ‖c' j - c' i‖

Tactic:
this j i inej.symm (le_of_not_ge hij)

Premises used: le_of_not_ge, Ne.symm
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
this :
  ∀ (i j : Fin N.succ) (inej : i ≠ j) (hij : ‖a.c i‖ ≤ ‖a.c j‖), (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
hij : ¬‖a.c i‖ ≤ ‖a.c j‖
⊢ 1 - δ ≤ ‖c' j - c' i‖

Tactic:
exact this j i inej.symm (le_of_not_ge hij)

Premises used: le_of_not_ge, Ne.symm
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
inl : ∀ (Hj : ‖a.c j‖ ≤ 2), 1 - δ ≤ ‖c' i - c' j‖
inr : ∀ (Hj : 2 < ‖a.c j‖), 1 - δ ≤ ‖c' i - c' j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
rcases le_or_gt ‖a.c j‖ 2 with (Hj | Hj)

Premises used: Norm.norm, Besicovitch.SatelliteConfig.c, le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : ‖a.c j‖ ≤ 2
inl : 1 - δ ≤ ‖a.c i - a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
simp_rw [c', Hj, hij.trans Hj, if_true]

Premises used: if_true, LE.le.trans
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : ‖a.c j‖ ≤ 2
⊢ 1 - δ ≤ ‖a.c i - a.c j‖

Tactic:
exists_normalized_aux1 a lastr hτ δ hδ1 hδ2 i j inej

Premises used: Besicovitch.SatelliteConfig.exists_normalized_aux1
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : ‖a.c j‖ ≤ 2
⊢ 1 - δ ≤ ‖a.c i - a.c j‖

Tactic:
exact exists_normalized_aux1 a lastr hτ δ hδ1 hδ2 i j inej

Premises used: Besicovitch.SatelliteConfig.exists_normalized_aux1
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
⊢ ‖a.c j‖ ≤ 2 ↔ False

Tactic:
simpa only [not_le, iff_false] using Hj

Premises used: not_le, iff_false
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
⊢ ‖a.c j‖ ≤ 2 ↔ False

Tactic:
have H'j : ‖a.c j‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hj
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
inr : ∀ (Hi : ‖a.c i‖ ≤ 2), 1 - δ ≤ ‖c' i - c' j‖
inr₁ : ∀ (Hi : 2 < ‖a.c i‖), 1 - δ ≤ ‖c' i - c' j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
rcases le_or_gt ‖a.c i‖ 2 with (Hi | Hi)

Premises used: Norm.norm, Besicovitch.SatelliteConfig.c, le_or_gt, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
inr : 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
simp_rw [c', Hi, if_true, H'j, if_false]

Premises used: if_true, if_false
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
⊢ 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
exists_normalized_aux2 a lastc lastr hτ δ hδ1 hδ2 i j inej Hi Hj

Premises used: Besicovitch.SatelliteConfig.exists_normalized_aux2
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : ‖a.c i‖ ≤ 2
⊢ 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
exact exists_normalized_aux2 a lastc lastr hτ δ hδ1 hδ2 i j inej Hi Hj

Premises used: Besicovitch.SatelliteConfig.exists_normalized_aux2
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
⊢ ‖a.c i‖ ≤ 2 ↔ False

Tactic:
simpa only [not_le, iff_false] using Hi

Premises used: not_le, iff_false
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
⊢ ‖a.c i‖ ≤ 2 ↔ False

Tactic:
have H'i : ‖a.c i‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hi
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
H'i : ‖a.c i‖ ≤ 2 ↔ False
inr : 1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
⊢ 1 - δ ≤ ‖c' i - c' j‖

Tactic:
simp_rw [c', H'i, if_false, H'j, if_false]

Premises used: if_false
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
H'i : ‖a.c i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
exists_normalized_aux3 a lastc lastr hτ δ hδ1 i j inej Hi hij

Premises used: Besicovitch.SatelliteConfig.exists_normalized_aux3
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun (i : Fin N.succ) ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
H'i : ‖a.c i‖ ≤ 2 ↔ False
⊢ 1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
exact exists_normalized_aux3 a lastc lastr hτ δ hδ1 i j inej Hi hij

Premises used: Besicovitch.SatelliteConfig.exists_normalized_aux3
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
rcases :
  ∀ (c' : Fin (multiplicity E).succ → E) (c'_le_two : ∀ (n : Fin (multiplicity E).succ), ‖c' n‖ ≤ 2)
    (hc' : Pairwise fun (i j : Fin (multiplicity E).succ) ↦ 1 - goodδ E ≤ ‖c' i - c' j‖), False
⊢ False

Tactic:
rcases b.exists_normalized a.centerAndRescale_center a.centerAndRescale_radius
        (one_lt_goodτ E).le (goodδ E) le_rfl (goodδ_lt_one E).le with
      ⟨c', c'_le_two, hc'⟩

Premises used: Besicovitch.SatelliteConfig.centerAndRescale_radius, le_rfl, Besicovitch.goodδ, LT.lt.le, Besicovitch.SatelliteConfig.centerAndRescale_center, Besicovitch.SatelliteConfig.exists_normalized, Besicovitch.one_lt_goodτ, Besicovitch.goodδ_lt_one
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
c' : Fin (multiplicity E).succ → E
c'_le_two : ∀ (n : Fin (multiplicity E).succ), ‖c' n‖ ≤ 2
hc' : Pairwise fun (i j : Fin (multiplicity E).succ) ↦ 1 - goodδ E ≤ ‖c' i - c' j‖
⊢ False

Tactic:
lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))

Premises used: Besicovitch.le_multiplicity_of_δ_of_fin, lt_irrefl, Nat.lt_succ_self, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
c' : Fin (multiplicity E).succ → E
c'_le_two : ∀ (n : Fin (multiplicity E).succ), ‖c' n‖ ≤ 2
hc' : Pairwise fun (i j : Fin (multiplicity E).succ) ↦ 1 - goodδ E ≤ ‖c' i - c' j‖
⊢ False

Tactic:
exact
      lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))

Premises used: Besicovitch.le_multiplicity_of_δ_of_fin, lt_irrefl, Nat.lt_succ_self, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ HasBesicovitchCovering E

Tactic:
⟨⟨multiplicity E, goodτ E, one_lt_goodτ E, isEmpty_satelliteConfig_multiplicity E⟩⟩

Premises used: HasBesicovitchCovering.mk, Besicovitch.goodτ, Besicovitch.multiplicity, And.intro, Exists.intro, Besicovitch.isEmpty_satelliteConfig_multiplicity, Besicovitch.one_lt_goodτ
-- Module: Mathlib.MeasureTheory.Covering.DensityTheorem
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : IsUnifLocDoublingMeasure μ
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
inst_5 : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
⊢ 0 < R

Tactic:
have Rpos : 0 < R := scalingScaleOf_pos _ _