no goals
α : Type u_1
E : Type u_2
F : Type ?u.232029
m0 : MeasurableSpace α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
h : NeBot (ae μ)
c : E
⊢ (⨍ (x : α), c ∂μ) = c
simp only [average_eq, integral_const, Measure.restrict_apply, MeasurableSet.univ, one_smul,
  univ_inter, smul_smul, ← ENNReal.toReal_inv, ← ENNReal.toReal_mul, ENNReal.inv_mul_cancel,
  measure_ne_top μ univ, Ne.def, measure_univ_eq_zero, ae_neBot.1 h, not_false_iff,
  ENNReal.one_toReal]