-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem measure_closedBall_div_le_integral [IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) :
    (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ x, f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ

Tactic:
have K_pos : 0 < K := by
  simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ (μ (closedBall c f.rIn)).toReal

Tactic:
rw [div_le_iff₀ (pow_pos K_pos _), addHaar_closedBall' _ _ f.rIn_pos.le,
  addHaar_closedBall' _ _ f.rOut_pos.le, ENNReal.toReal_mul, ENNReal.toReal_mul,
  ENNReal.toReal_ofReal (pow_nonneg f.rOut_pos.le _),
  ENNReal.toReal_ofReal (pow_nonneg f.rIn_pos.le _), mul_assoc, mul_comm _ (K ^ _), ← mul_assoc,
  ← mul_pow, mul_comm _ K]

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ f.rOut ^ finrank ℝ E * (μ (closedBall 0 1)).toReal ≤ (K * f.rIn) ^ finrank ℝ E * (μ (closedBall 0 1)).toReal

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ f.rOut ^ finrank ℝ E * (μ (closedBall 0 1)).toReal ≤ (K * f.rIn) ^ finrank ℝ E * (μ (closedBall 0 1)).toReal

Tactic:
gcongr

Result:
case h.ha
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ 0 ≤ f.rOut

Proof state:
case h.ha
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ 0 ≤ f.rOut

Tactic:
exact f.rOut_pos.le

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
⊢ 0 < K

Tactic:
simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ

Tactic:
apply le_trans _ (f.measure_closedBall_le_integral μ)

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsAddHaarMeasure
K : ℝ
h : f.rOut ≤ K * f.rIn
K_pos : 0 < K
⊢ (μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ (μ (closedBall c f.rIn)).toReal