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∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (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
grw : (↑t : ℝ≥0∞) ^ (1 + n) ≤ (↑t : ℝ≥0∞) * f x
grw₁ : HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 1 * (↑t : ℝ≥0∞) ^ n ≤ (↑t : ℝ≥0∞) * f x
grw₂ : (↑t : ℝ≥0∞) * (↑t : ℝ≥0∞) ^ n ≤ (↑t : ℝ≥0∞) * f x
⊢ (↑t : ℝ≥0∞) ^ (n + 1) ≤ (↑t : ℝ≥0∞) * f x
have grw₃ : (↑t : ℝ≥0∞) * f x ≤ (↑t : ℝ≥0∞) * f x
Tactic: grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, 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∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) ≤
    (↑t : ℝ≥0∞) * ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ
have ρ₁ : (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) ≤
  HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
Tactic: calc
      ρ (s ∩ f ⁻¹' I) ≤ (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        rw [← ENNReal.coe_zpow t_ne_zero']
        apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
        intro x hx
        apply hx.2.2.trans_le (le_of_eq _)
        rw [ENNReal.coe_zpow t_ne_zero']
      _ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ := by
        apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
      _ = t * ∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ := lintegral_const_mul _ f_meas
-- 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∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
ρ₁ :
  (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) ≤
    (↑t : ℝ≥0∞) * ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ
have ρ₂ : HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
  ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ
Tactic: calc
      ρ (s ∩ f ⁻¹' I) ≤ (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        rw [← ENNReal.coe_zpow t_ne_zero']
        apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
        intro x hx
        apply hx.2.2.trans_le (le_of_eq _)
        rw [ENNReal.coe_zpow t_ne_zero']
      _ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ := by
        apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
      _ = t * ∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ := lintegral_const_mul _ f_meas
-- 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∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
ρ₁ :
  (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
ρ₂ :
  HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
    ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ
⊢ (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) ≤
    (↑t : ℝ≥0∞) * ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ
have ρ₃ : ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ ≤ ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) * f x ∂μ
Tactic: calc
      ρ (s ∩ f ⁻¹' I) ≤ (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        rw [← ENNReal.coe_zpow t_ne_zero']
        apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
        intro x hx
        apply hx.2.2.trans_le (le_of_eq _)
        rw [ENNReal.coe_zpow t_ne_zero']
      _ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ := by
        apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
      _ = t * ∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ := lintegral_const_mul _ f_meas
-- 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∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have C : ∀ (n : ℤ),
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
Tactic: have C :
    ∀ n : ℤ,
      ρ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) ≤
        (t • ν) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
    intro n
    let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))
    have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)
    simp only [ν, I, M, withDensity_apply, coe_nnreal_smul_apply]
    calc
      ρ (s ∩ f ⁻¹' I) ≤ (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        rw [← ENNReal.coe_zpow t_ne_zero']
        apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
        intro x hx
        apply hx.2.2.trans_le (le_of_eq _)
        rw [ENNReal.coe_zpow t_ne_zero']
      _ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ := by
        apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
      _ = t * ∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ := lintegral_const_mul _ f_meas
-- 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ρ : ρ ≪ μ
⊢ μ.withDensity (v.limRatioMeas hρ) = ρ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- 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
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_antisymm ?_ ?_
-- 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
h :
  LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_antisymm ?_ ?_
-- 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
⊢ Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have refine_1 : Tendsto (fun (t : ℝ≥0) ↦ HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) (𝓝[>] 1) (𝓝 (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2))
Tactic: refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_
-- 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
refine_1 : Tendsto (fun (t : ℝ≥0) ↦ HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) (𝓝[>] 1) (𝓝 (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2))
⊢ Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have refine_2 : HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ 0 ∨ Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_
-- 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
refine_1 : Tendsto (fun (t : ℝ≥0) ↦ HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) (𝓝[>] 1) (𝓝 (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2))
refine_2 : HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ 0 ∨ Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have refine_3 : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ ∞
Tactic: refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_
-- 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
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this : Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
Tactic: have : Tendsto (fun t : ℝ≥0 =>
        ((t : ℝ≥0∞) ^ 2 * ρ s : ℝ≥0∞)) (𝓝[>] 1) (𝓝 ((1 : ℝ≥0∞) ^ 2 * ρ s)) := by
      refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_
      · exact ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)
      · simp
      · simp only [one_pow, Ne, or_true, ENNReal.one_ne_top, not_false_iff]
-- 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
this :
  Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this₁ : Tendsto (β := ℝ≥0∞)
  (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
Tactic: simp only [one_pow, one_mul] at this
Cleared hypotheses: this
-- 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
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
  (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine ge_of_tendsto this ?_
-- 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
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
    (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∀ (a : ℝ≥0) (ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a),
  (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑a : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin] with _ 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
⊢ Tendsto
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1)
    (𝓝
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have refine : Ne (α := ℝ≥0∞) 1 0 ∨ Ne (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_
-- 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
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this : Tendsto
  (fun (t : ℝ≥0) ↦
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (𝓝[>] 1)
  (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
Tactic: have :
      Tendsto (fun t : ℝ≥0 => (t : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s) (𝓝[>] 1)
        (𝓝 ((1 : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s)) := by
      refine ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_
      simp only [true_or, Ne, not_false_iff, one_ne_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
this :
  Tendsto
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1)
    (𝓝
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this₁ : Tendsto (β := ℝ≥0∞)
  (fun (t : ℝ≥0) ↦
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
Tactic: simp only [one_mul] at this
Cleared hypotheses: this
-- 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
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
  (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine ge_of_tendsto this ?_
-- 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
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
    (ρ : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∀ (a : ℝ≥0) (ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a),
  (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin] with _ ht