awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : β) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 (s.indicator 1 x))
have h : ∀ (a : β),
  Tendsto (β := ℝ≥0∞)
      (fun (a : Set β) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
      (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) a) (𝓝 (s.indicator 1 a)) →
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall a r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall a r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 (s.indicator 1 a))
Tactic: filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet
      (Besicovitch.vitaliFamily μ) hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
⊢ ∀ᵐ (x : β) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 1)
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Tendsto (β := ℝ≥0∞)
                  (fun (a : Set β) ↦
                    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
                      ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
                  (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 1))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Tendsto (β := ℝ≥0∞)
                  (fun (r : ℝ) ↦
                    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
                      ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
                  (𝓝[>] 0) (𝓝 1))
              x}
          x}
    a
Tactic: filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div (Besicovitch.vitaliFamily μ) s] with x
    hx using hx.comp (tendsto_filterAt μ x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Tendsto (β := ℝ≥0∞)
                    (fun (a : Set β) ↦
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
                        ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
                    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 1))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Tendsto (β := ℝ≥0∞)
                    (fun (r : ℝ) ↦
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
                        ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
                    (𝓝[>] 0) (𝓝 1))
                x}
            x}
      a
⊢ ∀ᵐ (x : β) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 1)
have h₁ : ∀ (a : β),
  Tendsto (β := ℝ≥0∞)
      (fun (a : Set β) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
      (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) a) (𝓝 1) →
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall a r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall a r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 1)
Tactic: filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div (Besicovitch.vitaliFamily μ) s] with x
    hx using hx.comp (tendsto_filterAt μ x)
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
⊢ (fun (i j : Fin N.succ) ↦
      (a.r (last N))⁻¹ * a.r i ≤
            dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c j - a.c (last N))) ∧
          (a.r (last N))⁻¹ * a.r j ≤ τ * ((a.r (last N))⁻¹ * a.r i) ∨
        (a.r (last N))⁻¹ * a.r j ≤
            dist ((a.r (last N))⁻¹ • (a.c j - a.c (last N))) ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ∧
          (a.r (last N))⁻¹ * a.r i ≤ τ * ((a.r (last N))⁻¹ * a.r j))
    i j
have simp : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
  (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Tactic: simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
      Real.norm_of_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 τ
i j : Fin N.succ
hij : i ≠ j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inl : ∀ (H₁ : a.r i ≤ dist (a.c i) (a.c j)) (H₂ : a.r j ≤ τ * a.r i),
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Tactic: rcases a.h hij with (⟨H₁, H₂⟩ | ⟨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 τ
i j : Fin N.succ
hij : i ≠ j
inl :
  ∀ (H₁ : a.r i ≤ dist (a.c i) (a.c j)) (H₂ : a.r j ≤ τ * a.r i),
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
        (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
        (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inr : ∀ (H₁ : a.r j ≤ dist (a.c j) (a.c i)) (H₂ : a.r i ≤ τ * a.r j),
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Tactic: rcases a.h hij with (⟨H₁, H₂⟩ | ⟨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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inl : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
  (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
Tactic: left
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inr : (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Tactic: right
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inl : ∀ (H₁ : a.r i ≤ dist (a.c i) (a.c j)) (H₂ : a.r j ≤ τ * a.r i),
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
Tactic: rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩) <;> [left; right]
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
inl :
  ∀ (H₁ : a.r i ≤ dist (a.c i) (a.c j)) (H₂ : a.r j ≤ τ * a.r i),
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inr : ∀ (H₁ : a.r j ≤ dist (a.c j) (a.c i)) (H₂ : a.r i ≤ τ * a.r j),
  (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Tactic: rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩) <;> [left; right]
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have inl : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)
Tactic: constructor
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
inl : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have inl₁ : (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
Tactic: constructor
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inr : (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)
Tactic: constructor
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
inr : (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inr₁ : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Tactic: constructor
-- 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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)
have inl : 0 ≤ (a.r (last N))⁻¹
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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have inl : 0 ≤ (a.r (last N))⁻¹
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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)
have inr : 0 ≤ (a.r (last N))⁻¹
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 τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
have inr : 0 ≤ (a.r (last N))⁻¹
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 τ
i : Fin (N + 1)
hi : i < last N
⊢ (a.r (last N))⁻¹ * a.r i ≤
      dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c (last N) - a.c (last N))) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ τ * ((a.r (last N))⁻¹ * a.r i)
have simp : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
  (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
Tactic: simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
      Real.norm_of_nonneg]
-- 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 τ
i : Fin (N + 1)
hi : i < last N
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
Tactic: have ⟨H₁, H₂⟩ := a.hlast i hi
-- 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 τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have H₂ : a.r (last N) ≤ τ * a.r i
Tactic: have ⟨H₁, H₂⟩ := a.hlast i 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 τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have left : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))
Tactic: constructor
-- 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 τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
left : (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have right : (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
Tactic: constructor
-- 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 τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))
have left : 0 ≤ (a.r (last N))⁻¹
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 τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)
have right : 0 ≤ (a.r (last N))⁻¹
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 τ
i : Fin (N + 1)
hi : i < last N
⊢ dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c (last N) - a.c (last N))) ≤
    (a.r (last N))⁻¹ * a.r i + (a.r (last N))⁻¹ * a.r (last N)
have simp : (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ≤ (a.r (last N))⁻¹ * (a.r i + a.r (last N))
Tactic: simp (disch := positivity) only [dist_smul₀, ← mul_add, dist_sub_right, Real.norm_of_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 τ
i : Fin (N + 1)
hi : i < last N
⊢ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ≤ (a.r (last N))⁻¹ * (a.r i + a.r (last N))
have hbc : dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ≤ HPow.hPow (α := ℕ) 5 (finrank ℝ E)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
⊢ s.card ≤ HPow.hPow (α := ℕ) 5 (finrank ℝ E)
have ρpos : 0 < ρ
Tactic: have ρpos : 0 < ρ := by norm_num
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
⊢ s.card ≤ HPow.hPow (α := ℕ) 5 (finrank ℝ E)
have hA : let A : Set E := ⋃ c ∈ s, ball c δ;
A = ⋃ c ∈ s, ball c δ
Tactic: set A := ⋃ c ∈ s, ball (c : E) δ with hA
-- 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
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
⊢ Function.onFun (β := Set E) Disjoint (fun (c : E) ↦ ball c δ) c d
have h₁ : δ + δ ≤ dist c d
Tactic: apply ball_disjoint_ball
-- 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
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
⊢ δ + δ ≤ dist c d
have h₁ : δ + δ ≤ ‖c - d‖
Tactic: rw [dist_eq_norm]
-- 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
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
c : E
hc : c ∈ (↑s : Set E)
d : E
hd : d ∈ (↑s : Set E)
hcd : c ≠ d
⊢ δ + δ ≤ ‖c - d‖
have h₁ : δ + δ = 1
Tactic: convert! h c hc d hd hcd
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
⊢ s.card ≤ HPow.hPow (α := ℕ) 5 (finrank ℝ E)
have D : (↑s : Set E).Pairwise (Function.onFun (β := Set E) Disjoint fun (c : E) ↦ ball c δ)
Tactic: have D : Set.Pairwise (s : Set E) (Disjoint on fun c => ball (c : E) δ) := by
    rintro c hc d hd hcd
    apply ball_disjoint_ball
    rw [dist_eq_norm]
    convert! h c hc d hd hcd
    norm_num