awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
x : E
⊢ f.normed μ x = (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
rfl

Premises used: ContDiffBump.normed, rfl
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
x : E
⊢ 0 ≤ f.normed μ x

Tactic:
div_nonneg f.nonneg <| integral_nonneg f.nonneg'

Premises used: MeasureTheory.integral_nonneg, ContDiffBump.normed, ContDiffBump.nonneg, div_nonneg, ContDiffBump.nonneg'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
n : ℕ∞
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (f.normed μ)

Tactic:
f.contDiff.div_const _

Premises used: ContDiff.div_const, ContDiffBump.normed, ContDiffBump.contDiff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (f.normed μ)

Tactic:
f.continuous.div_const _

Premises used: ContDiffBump.normed, Continuous.div_const, ContDiffBump.continuous
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ Integrable (↑f : E → ℝ) μ

Tactic:
f.continuous.integrable_of_hasCompactSupport f.hasCompactSupport

Premises used: Continuous.integrable_of_hasCompactSupport, ContDiffBump.hasCompactSupport, ContDiffBump.continuous
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ Integrable (f.normed μ) μ

Tactic:
f.integrable.div_const _

Premises used: ContDiffBump.integrable, ContDiffBump.normed, MeasureTheory.Integrable.div_const
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ LT.lt (α := ℝ) 0 (∫ (x : E), (↑f : E → ℝ) x ∂μ)

Tactic:
(integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr ?_

Premises used: Iff.mpr, ContDiffBump.integrable, MeasureTheory.integral_pos_iff_support_of_nonneg, ContDiffBump.nonneg'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
refine : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (support (↑f : E → ℝ)) : ENNReal)
⊢ LT.lt (α := ℝ) 0 (∫ (x : E), (↑f : E → ℝ) x ∂μ)

Tactic:
refine (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr ?_

Premises used: Iff.mpr, ContDiffBump.integrable, MeasureTheory.integral_pos_iff_support_of_nonneg, ContDiffBump.nonneg'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (ball c f.rOut) : ENNReal)
⊢ LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (support (↑f : E → ℝ)) : ENNReal)

Tactic:
rw [f.support_eq]

Premises used: ContDiffBump.support_eq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (ball c f.rOut) : ENNReal)

Tactic:
measure_ball_pos μ c f.rOut_pos

Premises used: Metric.measure_ball_pos, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set E) → ENNReal) (ball c f.rOut) : ENNReal)

Tactic:
exact measure_ball_pos μ c f.rOut_pos

Premises used: Metric.measure_ball_pos, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
simp_rw : HSMul.hSMul (α := ℝ) (β := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ)⁻¹ (∫ (x : E), (↑f : E → ℝ) x ∂μ) = 1
⊢ Eq (α := ℝ) (∫ (x : E), f.normed μ x ∂μ) 1

Tactic:
simp_rw [ContDiffBump.normed, div_eq_mul_inv, mul_comm (f _), ← smul_eq_mul, integral_smul]

Premises used: ContDiffBump.normed, MeasureTheory.integral_smul, div_eq_mul_inv, mul_comm, smul_eq_mul, ContDiffBump.toFun
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ)⁻¹ (∫ (x : E), (↑f : E → ℝ) x ∂μ) = 1

Tactic:
inv_mul_cancel₀ f.integral_pos.ne'

Premises used: LT.lt.ne', inv_mul_cancel₀, ContDiffBump.integral_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ)⁻¹ (∫ (x : E), (↑f : E → ℝ) x ∂μ) = 1

Tactic:
exact inv_mul_cancel₀ f.integral_pos.ne'

Premises used: LT.lt.ne', inv_mul_cancel₀, ContDiffBump.integral_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : (support (↑f : E → ℝ) ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
rw₁ : (ball c f.rOut ∩ support (M := ℝ) fun (x : E) ↦ ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut
rw₂ : ball c f.rOut ∩ univ = ball c f.rOut
rw₃ rw₄ : ball c f.rOut = ball c f.rOut
⊢ (support (M := ℝ) fun (x : E) ↦ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ) = ball c f.rOut

Tactic:
rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]

Premises used: Set.inter_univ, ContDiffBump.support_eq, LT.lt.ne', Function.support_const, Function.support_div, ContDiffBump.integral_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (f.normed μ)) = closedBall c f.rOut
rw₁ : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut
rw₂ rw₃ : closedBall c f.rOut = closedBall c f.rOut
⊢ tsupport (f.normed μ) = closedBall c f.rOut

Tactic:
rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']

Premises used: ContDiffBump.support_normed_eq, tsupport, LT.lt.ne', closure_ball, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
⊢ HasCompactSupport (f.normed μ)

Tactic:
simp only [HasCompactSupport, f.tsupport_normed_eq (μ := μ), isCompact_closedBall]

Premises used: ProperSpace.isCompact_closedBall, ContDiffBump.tsupport_normed_eq, HasCompactSupport
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε

Tactic:
simp_rw [NormedAddGroup.tendsto_nhds_zero, Real.norm_eq_abs,
    abs_eq_self.mpr (φ _).rOut_pos.le] at hφ

Premises used: Iff.mpr, LT.lt.le, NormedAddGroup.tendsto_nhds_zero, abs_eq_self, Real.norm_eq_abs, ContDiffBump.rOut_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
rw : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support (M := ℝ) fun (x_1 : E) ↦ (φ x).normed μ x_1) ∈ 𝒫 ball c i
⊢ Tendsto (fun (i : ι) ↦ support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) l (𝓝 c).smallSets

Tactic:
rw [nhds_basis_ball.smallSets.tendsto_right_iff]

Premises used: Filter.HasBasis.smallSets, Metric.nhds_basis_ball, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support (M := ℝ) fun (x_1 : E) ↦ (φ x).normed μ x_1) ∈ 𝒫 ball c i

Tactic:
fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
refine :
  ∀ (ε : ℝ) (hε : 0 < ε) (i : ι) (hi : (φ i).rOut < ε), (support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) ∈ 𝒫 ball c ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support (M := ℝ) fun (x_1 : E) ↦ (φ x).normed μ x_1) ∈ 𝒫 ball c i

Tactic:
refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
rw : ball c (φ i).rOut ∈ 𝒫 ball c ε
⊢ (support (M := ℝ) fun (x : E) ↦ (φ i).normed μ x) ∈ 𝒫 ball c ε

Tactic:
rw [(φ i).support_normed_eq]

Premises used: ContDiffBump.support_normed_eq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ ball c (φ i).rOut ∈ 𝒫 ball c ε

Tactic:
ball_subset_ball hi.le

Premises used: Set.Mem, setOf, Set.powerset, LT.lt.le, Metric.ball_subset_ball
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ ball c (φ i).rOut ∈ 𝒫 ball c ε

Tactic:
exact ball_subset_ball hi.le

Premises used: LT.lt.le, Metric.ball_subset_ball
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
X : Type u_2
inst_8 : NormedAddCommGroup X
inst_9 : NormedSpace ℝ X
inst_10 : CompleteSpace X
z : X
simp_rw : HSMul.hSMul (α := ℝ) (∫ (x : E), f.normed μ x ∂μ) z = z
simp_rw₁ : HSMul.hSMul (α := ℝ) 1 z = z
⊢ ∫ (x : E), f.normed μ x • z ∂μ = z

Tactic:
simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]

Premises used: ContDiffBump.integral_normed, integral_smul_const, one_smul
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ μ.real (closedBall c f.rIn) = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ Eq (α := ℝ) (∫ (x : E) in closedBall c f.rIn, 1 ∂μ) (∫ (x : E) in closedBall c f.rIn, (↑f : E → ℝ) x ∂μ)

Tactic:
setIntegral_congr_fun measurableSet_closedBall
        (fun x hx ↦ (one_of_mem_closedBall f hx).symm)

Premises used: MeasureTheory.setIntegral_congr_fun, ContDiffBump.one_of_mem_closedBall, measurableSet_closedBall, Eq.symm
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ LE.le (α := ℝ) (∫ (x : E) in closedBall c f.rIn, (↑f : E → ℝ) x ∂μ) (∫ (x : E), (↑f : E → ℝ) x ∂μ)

Tactic:
setIntegral_le_integral f.integrable (Eventually.of_forall (fun x ↦ f.nonneg))

Premises used: ContDiffBump.integrable, ContDiffBump.nonneg, MeasureTheory.setIntegral_le_integral, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
c₁ : μ.real (closedBall c f.rIn) = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ
⊢ μ.real (closedBall c f.rIn) ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
calc
  μ.real (closedBall c f.rIn) = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
  _ = ∫ x in closedBall c f.rIn, f x ∂μ := setIntegral_congr_fun measurableSet_closedBall
        (fun x hx ↦ (one_of_mem_closedBall f hx).symm)
  _ ≤ ∫ x, f x ∂μ := setIntegral_le_integral f.integrable (Eventually.of_forall (fun x ↦ f.nonneg))

Premises used: ContDiffBump.integrable, ContDiffBump.nonneg, MeasureTheory.Measure.real, MeasureTheory.setIntegral_le_integral, Filter.Eventually.of_forall, MeasureTheory.setIntegral_congr_fun, ContDiffBump.rIn, ContDiffBump.one_of_mem_closedBall, Metric.closedBall, measurableSet_closedBall, Eq.symm
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
hd : 0 < μ.real (closedBall c f.rIn)
hac : (↑f : E → ℝ) x ≤ 1
hdb : μ.real (closedBall c f.rIn) ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ
⊢ (↑f : E → ℝ) x / ∫ (x : E), (↑f : E → ℝ) x ∂μ ≤ 1 / μ.real (closedBall c f.rIn)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ 0 < μ.real (closedBall c f.rIn)

Tactic:
ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_pos, LT.lt.ne', Metric.measure_closedBall_pos, ContDiffBump.rIn_pos, MeasureTheory.measure_closedBall_lt_top, LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ 0 < μ.real (closedBall c f.rIn)

Tactic:
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne', Metric.measure_closedBall_pos, ContDiffBump.rIn_pos, MeasureTheory.measure_closedBall_lt_top, LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ (↑f : E → ℝ) x ≤ 1

Tactic:
f.le_one

Premises used: ContDiffBump.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ (↑f : E → ℝ) x ≤ 1

Tactic:
exact f.le_one

Premises used: ContDiffBump.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ μ.real (closedBall c f.rIn) ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
f.measure_closedBall_le_integral μ

Premises used: ContDiffBump.measure_closedBall_le_integral
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
inst_7 : μ.IsOpenPosMeasure
x : E
⊢ μ.real (closedBall c f.rIn) ≤ ∫ (x : E), (↑f : E → ℝ) x ∂μ

Tactic:
exact f.measure_closedBall_le_integral μ

Premises used: ContDiffBump.measure_closedBall_le_integral
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
apply : ∀ (x : E) (hx : x ∉ closedBall c f.rOut), (↑f : E → ℝ) x = 0
⊢ Eq (α := ℝ) (∫ (x : E), (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ)

Tactic:
apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero, Eq.symm
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
apply : f.rOut < dist x c
⊢ (↑f : E → ℝ) x = 0

Tactic:
apply f.zero_of_le_dist (le_of_lt _)

Premises used: le_of_lt, ContDiffBump.zero_of_le_dist
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ f.rOut < dist x c

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
apply : IntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (closedBall c f.rOut) μ
⊢ LE.le (α := ℝ) (∫ (x : E) in closedBall c f.rOut, (↑f : E → ℝ) x ∂μ) (∫ (x : E) in closedBall c f.rOut, 1 ∂μ)

Tactic:
apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)

Premises used: ContDiffBump.integrable, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono, ContDiffBump.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Normed
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : HasContDiffBump E
inst_3 : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
inst_6 : IsLocallyFiniteMeasure μ
⊢ IntegrableOn (ε := ℝ) (fun (x : E) ↦ 1) (closedBall c f.rOut) μ

Tactic:
simp [measure_closedBall_lt_top]

Premises used: MeasureTheory.measure_closedBall_lt_top