-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem withDensity_limRatioMeas_eq : μ.withDensity (v.limRatioMeas hρ) = ρ

Proof state:
case h
α : 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
this : Tendsto (fun t => ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (ρ s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑a✝ ^ 2 * ρ s

Tactic:
exact v.withDensity_le_mul hρ hs ht

Result:
no goals

Proof state:
case h
α : 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
⊢ (μ.withDensity (v.limRatioMeas hρ)) s = ρ s

Tactic:
refine le_antisymm ?_ ?_

Result:
case h.refine_1
α : 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
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s

case h.refine_2
α : 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
⊢ ρ s ≤ (μ.withDensity (v.limRatioMeas hρ)) s

Proof state:
case refine_3
α : 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
⊢ ρ s ≠ 0 ∨ 1 ^ 2 ≠ ⊤

Tactic:
simp only [one_pow, ENNReal.coe_one, Ne, or_true, ENNReal.one_ne_top, not_false_iff]

Result:
no goals

Proof state:
case h.refine_1
α : 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
this : Tendsto (fun t => ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (ρ s))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1, (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑c ^ 2 * ρ s

Tactic:
filter_upwards [self_mem_nhdsWithin] with _ ht

Result:
case h
α : 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
this : Tendsto (fun t => ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (ρ s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑a✝ ^ 2 * ρ s

Proof state:
case h.refine_2
α : 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
this :
  Tendsto (fun t => ↑t * (μ.withDensity (v.limRatioMeas hρ)) s) (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ)) s))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1, ρ s ≤ ↑c * (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
filter_upwards [self_mem_nhdsWithin] with _ ht

Result:
case h
α : 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
this :
  Tendsto (fun t => ↑t * (μ.withDensity (v.limRatioMeas hρ)) s) (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ)) s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ ρ s ≤ ↑a✝ * (μ.withDensity (v.limRatioMeas hρ)) s

Proof state:
case h.refine_2
α : 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
this :
  Tendsto (fun t => ↑t * (μ.withDensity (v.limRatioMeas hρ)) s) (𝓝[>] 1) (𝓝 (1 * (μ.withDensity (v.limRatioMeas hρ)) s))
⊢ ρ s ≤ (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
simp only [one_mul, ENNReal.coe_one] at this

Result:
case h.refine_2
α : 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
this :
  Tendsto (fun t => ↑t * (μ.withDensity (v.limRatioMeas hρ)) s) (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ)) s))
⊢ ρ s ≤ (μ.withDensity (v.limRatioMeas hρ)) s

Proof state:
case refine_1
α : 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
⊢ Tendsto (fun t => ↑t ^ 2) (𝓝[>] 1) (𝓝 (1 ^ 2))

Tactic:
exact ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)

Result:
no goals

Proof state:
case h.refine_1
α : 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
this : Tendsto (fun t => ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (1 ^ 2 * ρ s))
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s

Tactic:
simp only [one_pow, one_mul, ENNReal.coe_one] at this

Result:
case h.refine_1
α : 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
this : Tendsto (fun t => ↑t ^ 2 * ρ s) (𝓝[>] 1) (𝓝 (ρ s))
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s