awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ ContDiff.{0, u_1, 0} ℝ (E := E) ∞ u

Tactic:
(Classical.choose_spec (u_exists E)).1

Premises used: ExistsContDiffBumpBase.u_exists, Classical.choose_spec, And.left, ExistsContDiffBumpBase.u
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] u

Tactic:
(u_smooth E).continuous

Premises used: ContDiff.continuous, ExistsContDiffBumpBase.u_smooth
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ Eq.{u_1 + 1} (α := Set E) (support u) (ball 0 1)

Tactic:
(Classical.choose_spec (u_exists E)).2.2.1

Premises used: ExistsContDiffBumpBase.u_exists, Classical.choose_spec, And.right, And.left, ExistsContDiffBumpBase.u
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
rw : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ HasCompactSupport.{u_1, 0} (α := E) u

Tactic:
rw [hasCompactSupport_def, u_support, closure_ball (0 : E) one_ne_zero]

Premises used: ExistsContDiffBumpBase.u_support, hasCompactSupport_def, closure_ball, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ IsCompact.{u_1} (X := E) (closedBall 0 1)

Tactic:
isCompact_closedBall _ _

Premises used: ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ IsCompact.{u_1} (X := E) (closedBall 0 1)

Tactic:
exact isCompact_closedBall _ _

Premises used: ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
⊢ 0 ≤ u x

Tactic:
((Classical.choose_spec (u_exists E)).2.1 x).1

Premises used: ExistsContDiffBumpBase.u_exists, Classical.choose_spec, And.right, And.left, ExistsContDiffBumpBase.u
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
⊢ u x ≤ 1

Tactic:
((Classical.choose_spec (u_exists E)).2.1 x).2

Premises used: ExistsContDiffBumpBase.u_exists, Classical.choose_spec, And.right, And.left, ExistsContDiffBumpBase.u
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
⊢ u (-x) = u x

Tactic:
(Classical.choose_spec (u_exists E)).2.2.2 x

Premises used: ExistsContDiffBumpBase.u_exists, Classical.choose_spec, And.right, ExistsContDiffBumpBase.u
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ LT.lt (α := ℝ) 0 (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x)

Tactic:
(integral_pos_iff_support_of_nonneg u_nonneg ?_).mpr ?_

Premises used: Iff.mpr, MeasureTheory.integral_pos_iff_support_of_nonneg, ExistsContDiffBumpBase.u_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
refine_1 : @Integrable.{0, u_1} _ _ _ E inst_3 u μ
refine_2 : LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (support u) : ENNReal)
⊢ LT.lt (α := ℝ) 0 (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x)

Tactic:
refine (integral_pos_iff_support_of_nonneg u_nonneg ?_).mpr ?_

Premises used: Iff.mpr, MeasureTheory.integral_pos_iff_support_of_nonneg, ExistsContDiffBumpBase.u_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ @Integrable.{0, u_1} _ _ _ E inst_3 u μ

Tactic:
(u_continuous E).integrable_of_hasCompactSupport (u_compact_support E)

Premises used: ExistsContDiffBumpBase.u_continuous, Continuous.integrable_of_hasCompactSupport, ExistsContDiffBumpBase.u_compact_support
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ @Integrable.{0, u_1} _ _ _ E inst_3 u μ

Tactic:
exact (u_continuous E).integrable_of_hasCompactSupport (u_compact_support E)

Premises used: ExistsContDiffBumpBase.u_continuous, Continuous.integrable_of_hasCompactSupport, ExistsContDiffBumpBase.u_compact_support
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
refine_2 : LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (ball 0 1) : ENNReal)
⊢ LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (support u) : ENNReal)

Tactic:
rw [u_support]

Premises used: ExistsContDiffBumpBase.u_support
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (ball 0 1) : ENNReal)

Tactic:
measure_ball_pos _ _ zero_lt_one

Premises used: zero_lt_one, Metric.measure_ball_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (ball 0 1) : ENNReal)

Tactic:
exact measure_ball_pos _ _ zero_lt_one

Premises used: zero_lt_one, Metric.measure_ball_pos
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
h : ∀ (x : E), w D x = ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)
⊢ Eq.{u_1 + 1} (α := (x : E) → ℝ) (w D) fun (x : E) ↦
    ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
⊢ w D x = ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
apply : 0 ≤ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹
⊢ 0 ≤ w D x

Tactic:
apply mul_nonneg _ (u_nonneg _)

Premises used: mul_nonneg, ExistsContDiffBumpBase.u_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
apply : 0 ≤ (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E
⊢ 0 ≤ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹

Tactic:
apply inv_nonneg.2

Premises used: Iff.mpr, inv_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
apply : 0 ≤ |D| ^ finrank ℝ E
⊢ 0 ≤ (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E

Tactic:
apply mul_nonneg (u_int_pos E).le

Premises used: mul_nonneg, ExistsContDiffBumpBase.u_int_pos, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
⊢ 0 ≤ |D| ^ finrank ℝ E

Tactic:
apply pow_nonneg (abs_nonneg D)

Premises used: pow_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x y : E
⊢ ∀ (a : E), Membership.mem (γ := Set E) (closedBall 0 1) a → LE.le (α := ℝ) 0 1

Tactic:
simp only [zero_le_one, imp_true_iff]

Premises used: zero_le_one, imp_true_iff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
simp_rw :
  HSMul.hSMul (β := ℝ) ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹
      (@integral _ _ _ _ inst_3 μ fun (a : E) ↦ u (D⁻¹ • a)) =
    1
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ w D x) 1

Tactic:
simp_rw [w, integral_smul]

Premises used: MeasureTheory.integral_smul, ExistsContDiffBumpBase.w
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
rw :
  (D ^ finrank ℝ E * @integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x)⁻¹ •
      HSMul.hSMul (β := ℝ) (D ^ finrank ℝ E) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) =
    1
⊢ HSMul.hSMul (β := ℝ) ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹
      (@integral _ _ _ _ inst_3 μ fun (a : E) ↦ u (D⁻¹ • a)) =
    1

Tactic:
rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le, abs_of_nonneg Dpos.le, mul_comm]

Premises used: MeasureTheory.Measure.integral_comp_inv_smul_of_nonneg, LT.lt.le, ExistsContDiffBumpBase.u, mul_comm, abs_of_nonneg, MeasureTheory.Measure.addHaar
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ (D ^ finrank ℝ E * @integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x)⁻¹ •
      HSMul.hSMul (β := ℝ) (D ^ finrank ℝ E) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) =
    1

Tactic:
simp [field, (u_int_pos E).ne']

Premises used: ExistsContDiffBumpBase.u_int_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
rw : Eq.{u_1 + 1} (α := Set E) (ball 0 ‖D‖) (ball 0 D)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set E) (ball 0 D) (ball 0 D)
⊢ HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D

Tactic:
rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]

Premises used: LT.lt.le, LT.lt.ne', smul_unitBall, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D

Tactic:
have B : D • ball (0 : E) 1 = ball 0 D := by
    rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
B : HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D
⊢ ¬D ^ finrank ℝ E = 0

Tactic:
pow_ne_zero _ Dpos.ne'

Premises used: pow_ne_zero, LT.lt.ne'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
B : HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D
⊢ ¬D ^ finrank ℝ E = 0

Tactic:
exact pow_ne_zero _ Dpos.ne'

Premises used: pow_ne_zero, LT.lt.ne'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
B : HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D
⊢ D ^ finrank ℝ E ≠ 0

Tactic:
have C : D ^ finrank ℝ E ≠ 0 := by
    norm_cast
    exact pow_ne_zero _ Dpos.ne'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
B : HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D
C : D ^ finrank ℝ E ≠ 0
⊢ Eq.{u_1 + 1} (α := Set E) (support (w D)) (ball 0 D)

Tactic:
simp only [w_def, smul_eq_mul, support_mul, support_inv, univ_inter,
    support_comp_inv_smul₀ Dpos.ne', u_support, B, support_const (u_int_pos E).ne', support_const C,
    abs_of_nonneg Dpos.le]

Premises used: ExistsContDiffBumpBase.u_support, support_comp_inv_smul₀, ExistsContDiffBumpBase.u_int_pos, LT.lt.le, Set.univ_inter, LT.lt.ne', Function.support_inv, ExistsContDiffBumpBase.w_def, Function.support_const, abs_of_nonneg, Function.support_mul, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
rw : IsCompact.{u_1} (X := E) (closedBall 0 D)
⊢ HasCompactSupport.{u_1, 0} (α := E) (w D)

Tactic:
rw [hasCompactSupport_def, w_support E Dpos, closure_ball (0 : E) Dpos.ne']

Premises used: ExistsContDiffBumpBase.w_support, LT.lt.ne', hasCompactSupport_def, closure_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ IsCompact.{u_1} (X := E) (closedBall 0 D)

Tactic:
isCompact_closedBall _ _

Premises used: ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ IsCompact.{u_1} (X := E) (closedBall 0 D)

Tactic:
exact isCompact_closedBall _ _

Premises used: ProperSpace.isCompact_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
h1 : ∀ᵐ (x : E) ∂μ, w D (-x) = w D x
h2 : ∀ᵐ (x : E) ∂μ, φ (-x) = φ x
⊢ y D (-x) = y D x

Tactic:
apply convolution_neg_of_neg_eq

Premises used: MeasureTheory.convolution_neg_of_neg_eq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
h1 : ∀ (x : E), w D (-x) = w D x
⊢ ∀ᵐ (x : E) ∂μ, w D (-x) = w D x

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x_1 x : E
⊢ w D (-x) = w D x

Tactic:
simp only [w_def, mul_inv_rev, smul_neg, u_neg, smul_eq_mul]

Premises used: ExistsContDiffBumpBase.u_neg, smul_neg, ExistsContDiffBumpBase.w_def, mul_inv_rev, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
h2 : ∀ (x : E), φ (-x) = φ x
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x_1 x : E
⊢ φ (-x) = φ x

Tactic:
simp only [φ, indicator, mem_closedBall, dist_zero_right, norm_neg]

Premises used: Set.indicator, norm_neg, ExistsContDiffBumpBase.φ, Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
h : D + dist x 0 ≤ 1
⊢ ball x D ⊆ ball 0 1

Tactic:
apply ball_subset_ball'

Premises used: Metric.ball_subset_ball'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
⊢ dist x 0 ≤ 1 - D

Tactic:
simp only [mem_closedBall] at hx

Premises used: Metric.mem_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : dist x 0 ≤ 1 - D
linarith : 1 < D + dist x 0 → 1 - (D + dist x 0) + (dist x 0 - (1 - D)) = 0
⊢ D + dist x 0 ≤ 1

Tactic:
linarith only [hx]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
⊢ ball x D ⊆ ball 0 1

Tactic:
have C : ball x D ⊆ ball 0 1 := by
      apply ball_subset_ball'
      simp only [mem_closedBall] at hx
      linarith only [hx]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
simp : 1 < dist y 0 → False
⊢ φ y = 1

Tactic:
simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]

Premises used: not_le, ite_eq_left_iff, Set.indicator, zero_ne_one, ExistsContDiffBumpBase.φ, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
h'y : 1 < dist y 0
linarith : dist y 0 - 1 + (1 - dist y 0) = 0
⊢ False

Tactic:
linarith only [mem_ball.1 (C hy), h'y]

Premises used: Metric.mem_ball, Iff.mp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
have B : ∀ y : E, y ∈ ball x D → φ y = 1 := by
    have C : ball x D ⊆ ball 0 1 := by
      apply ball_subset_ball'
      simp only [mem_closedBall] at hx
      linarith only [hx]
    intro y hy
    simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]
    intro h'y
    linarith only [mem_ball.1 (C hy), h'y]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
B : ∀ y ∈ ball x D, φ y = 1
⊢ φ x = 1

Tactic:
have Bx : φ x = 1 := B _ (mem_ball_self Dpos)
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
rw : ∀ y ∈ ball x D, φ y = 1
⊢ ∀ y ∈ ball x D, φ y = φ x

Tactic:
rw [Bx]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
B
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
exact B
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = φ x

Tactic:
have B' : ∀ y, y ∈ ball x D → φ y = φ x := by rw [Bx]; exact B
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : Membership.mem (γ := Set E) (closedBall 0 (1 - D)) x
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ inst_3 μ fun (t : E) ↦
      (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (w D t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (φ x))
    1
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']

Premises used: MeasureTheory.convolution_eq_right', ExistsContDiffBumpBase.w_support, le_of_eq