awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
rwa : s / ‖a.c j‖ ≤ 1
⊢ 0 ≤ 1 - s / ‖a.c j‖
have rwa₁ : s ≤ 1 * ‖a.c j‖
Tactic: rwa [sub_nonneg, div_le_iff₀ (zero_lt_two.trans hj), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
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
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖
Tactic: have I : ‖a.c j - a.c i‖ ≤ ‖a.c j‖ - s + ‖d - a.c i‖ :=
    calc
      ‖a.c j - a.c i‖ ≤ ‖a.c j - d‖ + ‖d - a.c i‖ := by simp [← dist_eq_norm, dist_triangle]
      _ = ‖a.c j‖ - ‖a.c i‖ + ‖d - a.c i‖ := by
        nth_rw 1 [← one_smul ℝ (a.c j)]
        rw [add_left_inj, hd, ← sub_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg, sub_mul,
          one_mul, div_mul_cancel₀ _ (zero_le_two.trans_lt hj).ne']
        rwa [sub_nonneg, div_le_iff₀ (zero_lt_two.trans hj), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
⊢ a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
have inl : ∀ (H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j), a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
Tactic: rcases ah inej.symm with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
inl : ∀ (H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j), a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
⊢ a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
have inr : ∀ (H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i), a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
Tactic: rcases ah inej.symm with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
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‖
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
⊢ a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
have H₁ : a.r i ≤ ‖a.c j - a.c i‖ ∧ a.r j ≤ τ * a.r i
Tactic: rw [norm_sub_rev] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
H : a.r i ≤ ‖a.c j - a.c i‖ ∧ a.r j ≤ τ * a.r i
⊢ a.r i * (τ - 1) ≤ s * (τ - 1)
have ha : 0 ≤ τ - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
H : a.r i ≤ ‖a.c j - a.c i‖ ∧ a.r j ≤ τ * a.r i
⊢ a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
have j₁ : τ * a.r i - a.r i = a.r i * (τ - 1)
Tactic: calc
            a.r j - ‖a.c j - a.c i‖ ≤ τ * a.r i - a.r i := sub_le_sub H.2 H.1
            _ = a.r i * (τ - 1) := by ring
            _ ≤ s * (τ - 1) := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
H : a.r i ≤ ‖a.c j - a.c i‖ ∧ a.r j ≤ τ * a.r i
j₁ : τ * a.r i - a.r i = a.r i * (τ - 1)
⊢ a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1)
have j₂ : a.r i * (τ - 1) ≤ s * (τ - 1)
Tactic: calc
            a.r j - ‖a.c j - a.c i‖ ≤ τ * a.r i - a.r i := sub_le_sub H.2 H.1
            _ = a.r i * (τ - 1) := by ring
            _ ≤ s * (τ - 1) := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
⊢ s * (τ - 1) ≤ s * (δ / 2)
have hbc : τ - 1 ≤ δ / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
⊢ τ - 1 ≤ δ / 2
have linarith : δ / 2 < τ - 1 → 4 / 4 = 1
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
linarith : δ / 2 < τ - 1 → 4 / 4 = 1
⊢ τ - 1 ≤ δ / 2
have linarith₁ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
linarith : δ / 2 < τ - 1 → 4 / 4 = 1
linarith₁ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 4 = 4
⊢ τ - 1 ≤ δ / 2
have linarith₂ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 4 0
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
linarith : δ / 2 < τ - 1 → 4 / 4 = 1
linarith₁ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 4 0
⊢ τ - 1 ≤ δ / 2
have linarith₃ : δ / 2 < τ - 1 → 2 / 2 = 1
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
linarith : δ / 2 < τ - 1 → 4 / 4 = 1
linarith₁ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 4 0
linarith₃ : δ / 2 < τ - 1 → 2 / 2 = 1
⊢ τ - 1 ≤ δ / 2
have linarith₄ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
linarith : δ / 2 < τ - 1 → 4 / 4 = 1
linarith₁ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 4 0
linarith₃ : δ / 2 < τ - 1 → 2 / 2 = 1
linarith₄ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ τ - 1 ≤ δ / 2
have linarith₅ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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‖
linarith : δ / 2 < τ - 1 → 4 / 4 = 1
linarith₁ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 4 0
linarith₃ : δ / 2 < τ - 1 → 2 / 2 = 1
linarith₄ : δ / 2 < τ - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : δ / 2 < τ - 1 → GT.gt (α := ℝ) 2 0
⊢ τ - 1 ≤ δ / 2
have linarith₆ : δ / 2 < τ - 1 →
  2 * (1 * δ - (2 * τ - HMul.hMul (α := ℝ) 2 1)) + (0 - δ) + (4 * τ - (HMul.hMul (α := ℝ) 4 1 + 1 * δ)) = 0
Tactic: linarith only [δnonneg, hδ1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
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‖
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ
Tactic: have J : a.r j - ‖a.c j - a.c i‖ ≤ s / 2 * δ :=
    calc
      a.r j - ‖a.c j - a.c i‖ ≤ s * (τ - 1) := by
        rcases ah inej.symm with (H | H)
        · calc
            a.r j - ‖a.c j - a.c i‖ ≤ 0 := sub_nonpos.2 H.1
            _ ≤ s * (τ - 1) := mul_nonneg spos.le (sub_nonneg.2 hτ)
        · rw [norm_sub_rev] at H
          calc
            a.r j - ‖a.c j - a.c i‖ ≤ τ * a.r i - a.r i := sub_le_sub H.2 H.1
            _ = a.r i * (τ - 1) := by ring
            _ ≤ s * (τ - 1) := by gcongr
      _ ≤ s * (δ / 2) := by gcongr; linarith only [δnonneg, hδ1]
      _ = s / 2 * δ := by ring
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
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 * δ
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have invs_nonneg : 0 ≤ 2 / s
Tactic: have invs_nonneg : 0 ≤ 2 / s := div_nonneg zero_le_two (zero_le_two.trans hi.le)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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 / 2 - s / 2 * δ) ≤ 2 / s * ‖d - a.c i‖
have hbc : s / 2 - s / 2 * δ ≤ ‖d - a.c i‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
⊢ s / 2 - s / 2 * δ ≤ ‖d - a.c i‖
have linarith : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
Tactic: linarith only [hcrj, I, J, hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
linarith : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
⊢ s / 2 - s / 2 * δ ≤ ‖d - a.c i‖
have linarith₁ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith only [hcrj, I, J, hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
linarith : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
linarith₁ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ s / 2 - s / 2 * δ ≤ ‖d - a.c i‖
have linarith₂ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith only [hcrj, I, J, hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
linarith : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
linarith₁ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 2 1 = 2
⊢ s / 2 - s / 2 * δ ≤ ‖d - a.c i‖
have linarith₃ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → GT.gt (α := ℝ) 2 0
Tactic: linarith only [hcrj, I, J, hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
linarith : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
linarith₁ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → GT.gt (α := ℝ) 2 0
linarith₄ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
linarith₅ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → 2 / 2 = 1
linarith₇ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₉ : ‖d - a.c i‖ < s / 2 - s / 2 * δ → GT.gt (α := ℝ) 2 0
⊢ s / 2 - s / 2 * δ ≤ ‖d - a.c i‖
have linarith₁₀ : ‖d - a.c i‖ < s / 2 - s / 2 * δ →
  2 * ‖d - a.c i‖ - (1 * s - 1 * s * (1 * δ)) + 2 * (‖a.c j‖ - (a.r j + 1)) +
          2 * (‖a.c j - a.c i‖ - (‖a.c j‖ - s + ‖d - a.c i‖)) +
        (2 * a.r j - 2 * ‖a.c j - a.c i‖ - 1 * s * (1 * δ)) +
      (2 - s) =
    0
Tactic: linarith only [hcrj, I, J, hi]