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
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 * ‖d - a.c i‖
have rw : |2 / s| * ‖a.c i - d‖
Tactic: rw [norm_sub_rev, ← abs_of_nonneg invs_nonneg]
-- 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 * ‖d - a.c i‖ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have conv_lhs : |2 / s| * ‖a.c i - d‖ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
Tactic: conv_lhs => rw [norm_sub_rev, ← abs_of_nonneg invs_nonneg]
-- 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| * ‖a.c i - d‖ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have rw : ‖(2 / s) • a.c i - (2 / s * (s / ‖a.c j‖)) • a.c j‖ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
Tactic: rw [← Real.norm_eq_abs, ← norm_smul, smul_sub, hd, smul_smul]
-- 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) • a.c i - (2 / s * (s / ‖a.c j‖)) • a.c j‖ = ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have e_a : 2 / s * (s / ‖a.c j‖) = 2 / ‖a.c j‖
Tactic: congr 3
-- 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
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have δ₁ : 1 - δ = 2 / s * (s / 2 - s / 2 * δ)
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
-- 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
δ₁ : 1 - δ = 2 / s * (s / 2 - s / 2 * δ)
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have δ₂ : 2 / s * (s / 2 - s / 2 * δ) ≤ 2 / s * ‖d - a.c i‖
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
-- 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
δ₁ : 1 - δ = 2 / s * (s / 2 - s / 2 * δ)
δ₂ : 2 / s * (s / 2 - s / 2 * δ) ≤ 2 / s * ‖d - a.c i‖
⊢ 1 - δ ≤ ‖(2 / s) • a.c i - (2 / ‖a.c j‖) • a.c j‖
have δ₃ : 2 / s * ‖d - a.c i‖ = ‖(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
-- 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
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
⊢ ‖if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i‖ ≤ 2
have pos : ∀ (h : ‖a.c i‖ ≤ 2), ‖a.c i‖ ≤ 2
Tactic: split_ifs with 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
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
⊢ ‖if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i‖ ≤ 2
have neg : ∀ (h : ¬‖a.c i‖ ≤ 2), ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
Tactic: split_ifs with 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
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
⊢ ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
have pos : ∀ (hi : ‖a.c i‖ = 0), ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
Tactic: by_cases hi : ‖a.c i‖ = 0
-- 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
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
⊢ ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
have neg : ∀ (hi : ¬‖a.c i‖ = 0), ‖(2 / ‖a.c i‖) • a.c i‖ ≤ 2
Tactic: by_cases hi : ‖a.c i‖ = 0
-- 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
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
⊢ ∃ (c' : Fin N.succ → E), (∀ (n : Fin N.succ), ‖c' n‖ ≤ 2) ∧ Pairwise fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖
have norm_c'_le : ∀ (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]
-- 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
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‖
have refine : ∀ (i j : Fin N.succ) (inej : i ≠ j), (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
Tactic: refine ⟨c', fun n => norm_c'_le n, fun i j inej => ?_⟩
-- 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
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
⊢ (fun (i j : Fin N.succ) ↦ 1 - δ ≤ ‖c' i - c' j‖) i j
have 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‖
Tactic: wlog hij : ‖a.c i‖ ≤ ‖a.c j‖ generalizing i j
-- 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
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‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have wlog : ∀ (i j : Fin N.succ) (inej : i ≠ j) (hij : ‖a.c i‖ ≤ ‖a.c j‖), 1 - δ ≤ ‖c' i - c' j‖
Tactic: wlog hij : ‖a.c i‖ ≤ ‖a.c j‖ generalizing i j
Cleared hypotheses: i, j, inej
-- 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
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' i - c' j‖
have inr : 1 - δ ≤ ‖c' j - c' i‖
Tactic: rw [norm_sub_rev]
-- 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
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‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have inl : ∀ (Hj : ‖a.c j‖ ≤ 2), 1 - δ ≤ ‖c' i - c' j‖
Tactic: rcases le_or_gt ‖a.c j‖ 2 with (Hj | Hj)
-- 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
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‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have inr : ∀ (Hj : 2 < ‖a.c j‖), 1 - δ ≤ ‖c' i - c' j‖
Tactic: rcases le_or_gt ‖a.c j‖ 2 with (Hj | Hj)
-- 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
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 - δ ≤ ‖c' i - c' j‖
have inl : 1 - δ ≤ ‖a.c i - a.c j‖
Tactic: simp_rw [c', Hj, hij.trans Hj, if_true]
-- 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
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‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have H'j : ‖a.c j‖ ≤ 2 ↔ False
Tactic: have H'j : ‖a.c j‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using Hj
-- 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
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
⊢ 1 - δ ≤ ‖c' i - c' j‖
have inr : ∀ (Hi : ‖a.c i‖ ≤ 2), 1 - δ ≤ ‖c' i - c' j‖
Tactic: rcases le_or_gt ‖a.c i‖ 2 with (Hi | 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
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‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have inr₁ : ∀ (Hi : 2 < ‖a.c i‖), 1 - δ ≤ ‖c' i - c' j‖
Tactic: rcases le_or_gt ‖a.c i‖ 2 with (Hi | 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
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 - δ ≤ ‖c' i - c' j‖
have inr : 1 - δ ≤ ‖a.c i - (2 / ‖a.c j‖) • a.c j‖
Tactic: simp_rw [c', Hi, if_true, H'j, if_false]
-- 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
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‖
⊢ 1 - δ ≤ ‖c' i - c' j‖
have H'i : ‖a.c i‖ ≤ 2 ↔ False
Tactic: have H'i : ‖a.c i‖ ≤ 2 ↔ False := by simpa only [not_le, iff_false] using 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
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 - δ ≤ ‖c' i - c' j‖
have inr : 1 - δ ≤ ‖(2 / ‖a.c i‖) • a.c i - (2 / ‖a.c j‖) • a.c j‖
Tactic: simp_rw [c', H'i, if_false, H'j, if_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (goal)
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
⊢ False
have 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
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'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (hypothesis)
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)
⊢ VitaliFamily μ
have Rpos : 0 < R
Tactic: have Rpos : 0 < R := scalingScaleOf_pos _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
Rpos : 0 < R
x : α
⊢ ∃ᶠ (r : ℝ) in 𝓝[>] 0,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * r)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x r) : ENNReal)
have apply : ∀ {U : Set ℝ} (hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U),
  ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)
Tactic: apply frequently_iff.2 fun {U} hU => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
⊢ ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)
have obtain : ∀ (ε : ℝ) (εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε) (hε : Ioc 0 ε ⊆ U),
  ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)
Tactic: obtain ⟨ε, εpos, hε⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.DensityTheorem (goal)
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)
Rpos : 0 < R
x : α
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (𝓝[>] 0) U
ε : ℝ
εpos : Membership.mem (γ := Set ℝ) (Ioi 0) ε
hε : Ioc 0 ε ⊆ U
⊢ ∃ x_1 ∈ U,
    (μ : (a : Set α) → ENNReal) (closedBall x (3 * x_1)) ≤
      HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
        ((μ : (a : Set α) → ENNReal) (closedBall x x_1) : ENNReal)
have refine : (μ : (a : Set α) → ENNReal) (closedBall x (3 * min ε R)) ≤
  HMul.hMul (β := ENNReal) (↑(scalingConstantOf μ (max (4 * K + 3) 3)) : ENNReal)
    ((μ : (a : Set α) → ENNReal) (closedBall x (min ε R)) : ENNReal)
Tactic: refine ⟨min ε R, hε ⟨lt_min εpos Rpos, min_le_left _ _⟩, ?_⟩