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
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
ha : 0 ≤ 1 - δ / 4
⊢ (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4)

Tactic:
gcongr
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
⊢ (1 - δ / 4) * (1 + δ / 4) = 1 - HPow.hPow (β := ℕ) δ 2 / 16

Tactic:
ring
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
linarith : 1 < 1 - HPow.hPow (β := ℕ) δ 2 / 16 → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₁ : 1 < 1 - HPow.hPow (β := ℕ) δ 2 / 16 → 16 / 16 = 1
linarith₂ : 1 < 1 - HPow.hPow (β := ℕ) δ 2 / 16 → HMul.hMul (α := ℝ) 1 16 = 16
linarith₃ : 1 < 1 - HPow.hPow (β := ℕ) δ 2 / 16 → GT.gt (α := ℝ) 16 0
linarith₄ :
  1 < 1 - HPow.hPow (β := ℕ) δ 2 / 16 →
    HMul.hMul (α := ℝ) 16 1 - (HMul.hMul (α := ℝ) 16 1 - 1 * HPow.hPow (β := ℕ) (1 * δ) 2) +
        (0 - HPow.hPow (β := ℕ) δ 2) =
      0
⊢ 1 - HPow.hPow (β := ℕ) δ 2 / 16 ≤ 1

Tactic:
linarith only [sq_nonneg δ]

Premises used: sq_nonneg
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
⊢ (1 - δ / 4) * τ ≤ 1

Tactic:
have J : (1 - δ / 4) * τ ≤ 1 :=
    calc
      (1 - δ / 4) * τ ≤ (1 - δ / 4) * (1 + δ / 4) := by gcongr
      _ = (1 : ℝ) - δ ^ 2 / 16 := by ring
      _ ≤ 1 := by linarith only [sq_nonneg δ]
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
inl : ∀ (H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j), a.r j - δ ≤ ‖a.c i - a.c j‖
inr : ∀ (H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i), a.r j - δ ≤ ‖a.c i - a.c j‖
⊢ a.r j - δ ≤ ‖a.c i - a.c j‖

Tactic:
rcases ah inej.symm with (H | H)

Premises used: 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
inl : a.r j - δ ≤ ‖a.c j - a.c i‖
⊢ a.r j - δ ≤ ‖a.c i - a.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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
linarith : ‖a.c j - a.c i‖ < a.r j - δ → 4 / 4 = 1
linarith₁ : ‖a.c j - a.c i‖ < a.r j - δ → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : ‖a.c j - a.c i‖ < a.r j - δ → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : ‖a.c j - a.c i‖ < a.r j - δ → GT.gt (α := ℝ) 4 0
linarith₄ : ‖a.c j - a.c i‖ < a.r j - δ → 4 / 4 = 1
linarith₅ : ‖a.c j - a.c i‖ < a.r j - δ → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ‖a.c j - a.c i‖ < a.r j - δ → GT.gt (α := ℝ) 4 0
linarith₇ : ‖a.c j - a.c i‖ < a.r j - δ → 4 / 4 = 1
linarith₈ : ‖a.c j - a.c i‖ < a.r j - δ → HMul.hMul (α := ℝ) 1 4 = 4
linarith₉ : ‖a.c j - a.c i‖ < a.r j - δ → GT.gt (α := ℝ) 4 0
linarith₁₀ :
  ‖a.c j - a.c i‖ < a.r j - δ →
    4 * (1 - τ) + (4 * τ - (HMul.hMul (α := ℝ) 4 1 + 1 * δ)) + (a.r j - ‖a.c j - a.c i‖) +
        (‖a.c j - a.c i‖ - (a.r j - δ)) =
      0
linarith₁₁ : ‖a.c j - a.c i‖ < a.r j - δ → GT.gt (α := ℝ) 4 0
⊢ a.r j - δ ≤ ‖a.c j - a.c i‖

Tactic:
linarith [H.1]

Premises used: And.left
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
ha : 0 ≤ τ
⊢ τ * a.r i ≤ τ * 2

Tactic:
gcongr
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
hbc : τ ≤ 5 / 4
⊢ τ * 2 ≤ 5 / 4 * 2

Tactic:
gcongr
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
linarith : 5 / 4 < τ → 4 / 4 = 1
linarith₁ : 5 / 4 < τ → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 5 / 4 < τ → GT.gt (α := ℝ) 4 0
linarith₃ : 5 / 4 < τ → 4 / 4 = 1
linarith₄ : 5 / 4 < τ → HMul.hMul (α := ℝ) 1 4 = 4
linarith₅ : 5 / 4 < τ → GT.gt (α := ℝ) 4 0
linarith₆ : 5 / 4 < τ → HMul.hMul (α := ℝ) 1 5 - 4 * τ + (4 * τ - (HMul.hMul (α := ℝ) 4 1 + 1 * δ)) + (δ - 1) = 0
⊢ τ ≤ 5 / 4

Tactic:
linarith only [hδ1, hδ2]
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
⊢ 5 / 4 * 2 ≤ 4

Tactic:
norm_num
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
⊢ a.r j ≤ 4

Tactic:
have C : a.r j ≤ 4 :=
      calc
        a.r j ≤ τ * a.r i := H.2
        _ ≤ τ * 2 := by gcongr
        _ ≤ 5 / 4 * 2 := by gcongr; linarith only [hδ1, hδ2]
        _ ≤ 4 := by norm_num
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
h : a.r j / 4 * δ ≤ δ
⊢ a.r j - δ ≤ a.r j - a.r j / 4 * δ

Tactic:
gcongr _ - ?_
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
linarith : 1 < a.r j / 4 → 4 / 4 = 1
linarith₁ : 1 < a.r j / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 1 < a.r j / 4 → GT.gt (α := ℝ) 4 0
linarith₃ : 1 < a.r j / 4 → HMul.hMul (α := ℝ) 4 1 - 1 * a.r j + (a.r j - 4) = 0
⊢ a.r j / 4 ≤ 1

Tactic:
linarith 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r j / 4 * δ ≤ δ

Tactic:
exact mul_le_of_le_one_left δnonneg (by linarith only [C])

Premises used: mul_le_of_le_one_left
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r j - a.r j / 4 * δ = (1 - δ / 4) * a.r j

Tactic:
ring
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
hbc : a.r j ≤ τ * a.r i
⊢ (1 - δ / 4) * a.r j ≤ (1 - δ / 4) * (τ * 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 τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r j ≤ τ * a.r i

Tactic:
H.2

Premises used: And.right
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r j ≤ τ * a.r i

Tactic:
exact H.2

Premises used: And.right
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
rw : (1 - δ / 4) * τ * a.r i ≤ 1 * a.r i
⊢ (1 - δ / 4) * (τ * a.r i) ≤ 1 * a.r i

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
ha : 0 ≤ a.r i
⊢ (1 - δ / 4) * τ * a.r i ≤ 1 * 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 τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
rw : a.r i ≤ ‖a.c i - a.c j‖
⊢ 1 * a.r i ≤ ‖a.c i - a.c j‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r i ≤ ‖a.c i - a.c j‖

Tactic:
H.1

Premises used: And.left
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ a.r i ≤ ‖a.c i - a.c j‖

Tactic:
exact H.1

Premises used: And.left
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
j₁ : a.r j - δ ≤ a.r j - a.r j / 4 * δ
j₂ : a.r j - a.r j / 4 * δ = (1 - δ / 4) * a.r j
j₃ : (1 - δ / 4) * a.r j ≤ (1 - δ / 4) * (τ * a.r i)
j₄ : (1 - δ / 4) * (τ * a.r i) ≤ 1 * a.r i
j₅ : 1 * a.r i ≤ ‖a.c i - a.c j‖
⊢ a.r j - δ ≤ ‖a.c i - a.c j‖

Tactic:
calc
      a.r j - δ ≤ a.r j - a.r j / 4 * δ := by
        gcongr _ - ?_
        exact mul_le_of_le_one_left δnonneg (by linarith only [C])
      _ = (1 - δ / 4) * a.r j := by ring
      _ ≤ (1 - δ / 4) * (τ * a.r i) := by gcongr; exact H.2
      _ ≤ 1 * a.r i := by rw [← mul_assoc]; gcongr
      _ ≤ ‖a.c i - a.c j‖ := by rw [one_mul]; exact H.1

Premises used: HMul.hMul, Besicovitch.SatelliteConfig.c, HSub.hSub, HDiv.hDiv, Besicovitch.SatelliteConfig.r, 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
⊢ a.r j - δ ≤ ‖a.c i - a.c j‖

Tactic:
have A : a.r j - δ ≤ ‖a.c i - a.c j‖ := by
    rcases ah inej.symm with (H | H); · rw [norm_sub_rev]; linarith [H.1]
    have C : a.r j ≤ 4 :=
      calc
        a.r j ≤ τ * a.r i := H.2
        _ ≤ τ * 2 := by gcongr
        _ ≤ 5 / 4 * 2 := by gcongr; linarith only [hδ1, hδ2]
        _ ≤ 4 := by norm_num
    calc
      a.r j - δ ≤ a.r j - a.r j / 4 * δ := by
        gcongr _ - ?_
        exact mul_le_of_le_one_left δnonneg (by linarith only [C])
      _ = (1 - δ / 4) * a.r j := by ring
      _ ≤ (1 - δ / 4) * (τ * a.r i) := by gcongr; exact H.2
      _ ≤ 1 * a.r i := by rw [← mul_assoc]; gcongr
      _ ≤ ‖a.c i - a.c j‖ := by rw [one_mul]; exact H.1
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : a.r j - δ ≤ ‖a.c i - a.c j‖
set :
  let d := (2 / ‖a.c j‖) • a.c j;
  ∀ (hd : d = (2 / ‖a.c j‖) • a.c j), 1 - δ ≤ ‖a.c i - d‖
⊢ 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖

Tactic:
set d := (2 / ‖a.c j‖) • a.c j with hd

Premises used: Norm.norm, Besicovitch.SatelliteConfig.c, 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : a.r j - δ ≤ ‖a.c i - a.c j‖
d : E := (2 / ‖a.c j‖) • a.c j
hd : d = (2 / ‖a.c j‖) • a.c j
⊢ ‖a.c i - a.c j‖ ≤ ‖a.c i - d‖ + ‖d - a.c j‖

Tactic:
simp only [← dist_eq_norm, dist_triangle]

Premises used: dist_triangle, dist_eq_norm
-- 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
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c 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 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
A : a.r j - δ ≤ ‖a.c i - a.c j‖
d : E := (2 / ‖a.c j‖) • a.c j
hd : d = (2 / ‖a.c j‖) • a.c j
bc : ‖d - a.c j‖ ≤ a.r j - 1
⊢ ‖a.c i - d‖ + ‖d - a.c j‖ ≤ ‖a.c i - d‖ + (a.r j - 1)

Tactic:
gcongr