-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem le_mul_withDensity {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht : 1 < t) :
    ρ s ≤ t * μ.withDensity (v.limRatioMeas hρ) s

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
⊢ ρ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (t • ν) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ρ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (t • ν) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ ↑t ^ (n + 1) ≤ ↑t * f x

Tactic:
rw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one]

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ ↑t * ↑t ^ n ≤ ↑t * f x

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
let f := v.limRatioMeas hρ

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
have t_ne_zero' : t ≠ 0 := (zero_lt_one.trans ht).ne'

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ s ∩ f ⁻¹' I ⊆ {x | v.limRatioMeas hρ x < ↑(t ^ (n + 1))}

Tactic:
intro x hx

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ x ∈ {x | v.limRatioMeas hρ x < ↑(t ^ (n + 1))}

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {⊤}) ≤ (t • ν) (s ∩ f ⁻¹' {⊤})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ ↑t * ↑t ^ n ≤ ↑t * f x

Tactic:
exact mul_le_mul_left' hx.2.1 _

Result:
no goals