awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
have a : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [withDensity_absolutelyContinuous μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
⊢ (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have B : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
  ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
Tactic: have B : ν (s ∩ f ⁻¹' {∞}) ≤ ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' {∞}) := by
    rw [withDensity_absolutelyContinuous μ]
    · exact zero_le
    · rw [← nonpos_iff_eq_zero]
      exact (measure_mono inter_subset_right).trans (v.measure_limRatioMeas_top hρ).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞)
        (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) :
      ℝ≥0∞)
have M : MeasurableSet (s ∩ f ⁻¹' I)
Tactic: have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞)
        (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) :
      ℝ≥0∞)
have simp : ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ ≤
  (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
Tactic: simp only [ν, I, M, withDensity_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
    HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2 *
      HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (2 + (n - 1))) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
Tactic: rw [← mul_assoc, ← ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (2 + (n - 1))) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
have e_a : n + 1 = 2 + (n - 1)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2 *
      HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
have bc : HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) ≤
  (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) ≤
    (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I)
have bc : HMul.hMul (β := ℝ≥0∞) (↑(t ^ (n - 1)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) ≤
  (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I)
Tactic: rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(t ^ (n - 1)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) ≤
    (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I)
have bc : s ∩ f ⁻¹' I ⊆ {x : α | (↑(t ^ (n - 1)) : ℝ≥0∞) < v.limRatioMeas hρ x}
Tactic: apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ Membership.mem (γ := Set α) {x : α | (↑(t ^ (n - 1)) : ℝ≥0∞) < v.limRatioMeas hρ x} x
have apply : (↑(t ^ (n - 1)) : ℝ≥0∞) < (↑t : ℝ≥0∞) ^ n
Tactic: apply lt_of_lt_of_le _ hx.2.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ (↑(t ^ (n - 1)) : ℝ≥0∞) < (↑t : ℝ≥0∞) ^ n
have rw : t ^ n * HPow.hPow (β := ℤ) t (-1) < t ^ n
Tactic: rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne', ENNReal.coe_lt_coe, sub_eq_add_neg,
          zpow_add₀ t_ne_zero']
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
| t ^ n
have rw : t ^ n * 1
Tactic: rw [← mul_one (t ^ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ t ^ n * HPow.hPow (β := ℤ) t (-1) < t ^ n
have conv_rhs : t ^ n * HPow.hPow (β := ℤ) t (-1) < t ^ n * 1
Tactic: conv_rhs => rw [← mul_one (t ^ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ t ^ n * HPow.hPow (β := ℤ) t (-1) < t ^ n * 1
have hbc : HPow.hPow (β := ℤ) t (-1) < 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ HPow.hPow (β := ℤ) t (-1) < 1
have hbc : t⁻¹ < 1
Tactic: rw [zpow_neg_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ ≤
    (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞)
      (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have x : ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ =
  HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
Tactic: calc
      (∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ) ≤ ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ :=
        lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => hx.2.2.le))
      _ = (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ = (t : ℝ≥0∞) ^ (2 : ℤ) * ((t : ℝ≥0∞) ^ (n - 1) * μ (s ∩ f ⁻¹' I)) := by
        rw [← mul_assoc, ← ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top]
        congr 2
        abel
      _ ≤ (t : ℝ≥0∞) ^ (2 : ℤ) * ρ (s ∩ f ⁻¹' I) := by
        gcongr
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne']
        apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
        intro x hx
        apply lt_of_lt_of_le _ hx.2.1
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne', ENNReal.coe_lt_coe, sub_eq_add_neg,
          zpow_add₀ t_ne_zero']
        conv_rhs => rw [← mul_one (t ^ n)]
        gcongr
        rw [zpow_neg_one]
        exact inv_lt_one_of_one_lt₀ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x :
  ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ =
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
⊢ ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ ≤
    (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞)
      (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have x₁ : HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
  HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2 *
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
Tactic: calc
      (∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ) ≤ ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ :=
        lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => hx.2.2.le))
      _ = (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ = (t : ℝ≥0∞) ^ (2 : ℤ) * ((t : ℝ≥0∞) ^ (n - 1) * μ (s ∩ f ⁻¹' I)) := by
        rw [← mul_assoc, ← ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top]
        congr 2
        abel
      _ ≤ (t : ℝ≥0∞) ^ (2 : ℤ) * ρ (s ∩ f ⁻¹' I) := by
        gcongr
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne']
        apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
        intro x hx
        apply lt_of_lt_of_le _ hx.2.1
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne', ENNReal.coe_lt_coe, sub_eq_add_neg,
          zpow_add₀ t_ne_zero']
        conv_rhs => rw [← mul_one (t ^ n)]
        gcongr
        rw [zpow_neg_one]
        exact inv_lt_one_of_one_lt₀ ht