awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
⊢ (f x + f (-x)) / 2 ≠ 0
have refine_3 : 0 < (f x + f (-x)) / 2
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
⊢ 0 < f x
have apply : f x ≠ 0
Tactic: apply lt_of_le_of_ne (B x).1 (Ne.symm _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
⊢ f x ≠ 0
have rwa : ∀ (hx : x ∈ support f), f x ≠ 0
Tactic: rwa [← f_support] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
⊢ 0 < (f x + f (-x)) / 2
have this : 0 < f x
Tactic: have : 0 < f x := by
        apply lt_of_le_of_ne (B x).1 (Ne.symm _)
        rwa [← f_support] at hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
this : 0 < f x
⊢ 0 < (f x + f (-x)) / 2
have linarith : (f x + f (-x)) / 2 ≤ 0 → 2 / 2 = 1
Tactic: linarith [(B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
this : 0 < f x
linarith : (f x + f (-x)) / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < (f x + f (-x)) / 2
have linarith₁ : (f x + f (-x)) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
this : 0 < f x
linarith : (f x + f (-x)) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (f x + f (-x)) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < (f x + f (-x)) / 2
have linarith₂ : (f x + f (-x)) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [(B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
this : 0 < f x
linarith : (f x + f (-x)) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (f x + f (-x)) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (f x + f (-x)) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < (f x + f (-x)) / 2
have linarith₃ : (f x + f (-x)) / 2 ≤ 0 → 0 - f x + (1 * f x + 1 * f (-x) - HMul.hMul (α := ℝ) 2 0) + (0 - f (-x)) = 0
Tactic: linarith [(B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
⊢ (f x + f (-x)) / 2 = 0
have I1 : x ∉ support f
Tactic: have I1 : x ∉ support f := by rwa [f_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
⊢ -x ∉ support f
have rw : -x ∉ ball 0 1
Tactic: rw [f_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
⊢ (f x + f (-x)) / 2 = 0
have I2 : -x ∉ support f
Tactic: have I2 : -x ∉ support f := by
        rw [f_support]
        simpa using hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
I2 : -x ∉ support f
⊢ (f x + f (-x)) / 2 = 0
have I1₁ : f x = 0
Tactic: simp only [mem_support, Classical.not_not] at I1 I2
Cleared hypotheses: I1, I2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
I2 : -x ∉ support f
I1₁ : f x = 0
⊢ (f x + f (-x)) / 2 = 0
have I2₁ : f (-x) = 0
Tactic: simp only [mem_support, Classical.not_not] at I1 I2
Cleared hypotheses: I1, I2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ HasCompactSupport.{u_1, 0} (α := E) u
have rw : IsCompact.{u_1} (X := E) (closedBall 0 1)
Tactic: rw [hasCompactSupport_def, u_support, closure_ball (0 : E) one_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
have refine_1 : @Integrable.{0, u_1} _ _ _ E inst_3 u μ
Tactic: refine (integral_pos_iff_support_of_nonneg u_nonneg ?_).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 μ
⊢ LT.lt (α := ℝ) 0 (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x)
have refine_2 : LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (support u) : ENNReal)
Tactic: refine (integral_pos_iff_support_of_nonneg u_nonneg ?_).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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) (support u) : ENNReal)
have refine_2 : LT.lt (α := ENNReal) (0 : ENNReal) (((μ : Measure E) : (a : Set E) → ENNReal) (ball 0 1) : ENNReal)
Tactic: rw [u_support]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 : ℝ
⊢ 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)
have h : ∀ (x : E), w D x = ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹ • u (D⁻¹ • x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 ≤ w D x
have apply : 0 ≤ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹
Tactic: apply mul_nonneg _ (u_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 ≤ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹
have apply : 0 ≤ (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E
Tactic: apply inv_nonneg.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 ≤ (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E
have apply : 0 ≤ |D| ^ finrank ℝ E
Tactic: apply mul_nonneg (u_int_pos E).le
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ Eq (α := ℝ) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ w D x) 1
have 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
Tactic: simp_rw [w, integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 (β := ℝ) ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |D| ^ finrank ℝ E)⁻¹
      (@integral _ _ _ _ inst_3 μ fun (a : E) ↦ u (D⁻¹ • a)) =
    1
have 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
Tactic: rw [integral_comp_inv_smul_of_nonneg μ (u : E → ℝ) Dpos.le, abs_of_nonneg Dpos.le, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
have rw : Eq.{u_1 + 1} (α := Set E) (ball 0 ‖D‖) (ball 0 D)
Tactic: rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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)
⊢ HSMul.hSMul (β := Set E) D (ball 0 1) = ball 0 D
have rw₁ : Eq.{u_1 + 1} (α := Set E) (ball 0 D) (ball 0 D)
Tactic: rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := Set E) (support (w D)) (ball 0 D)
have B : 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := Set E) (support (w D)) (ball 0 D)
have C : D ^ finrank ℝ E ≠ 0
Tactic: have C : D ^ finrank ℝ E ≠ 0 := by
    norm_cast
    exact pow_ne_zero _ Dpos.ne'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ HasCompactSupport.{u_1, 0} (α := E) (w D)
have rw : IsCompact.{u_1} (X := E) (closedBall 0 D)
Tactic: rw [hasCompactSupport_def, w_support E Dpos, closure_ball (0 : E) Dpos.ne']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ y D (-x) = y D x
have h1 : ∀ᵐ (x : E) ∂μ, w D (-x) = w D x
Tactic: apply convolution_neg_of_neg_eq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ y D (-x) = y D x
have h2 : ∀ᵐ (x : E) ∂μ, φ (-x) = φ x
Tactic: apply convolution_neg_of_neg_eq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ ∀ᵐ (x : E) ∂μ, w D (-x) = w D x
have h1 : ∀ (x : E), w D (-x) = w D x
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ ∀ᵐ (x : E) ∂μ, φ (-x) = φ x
have h2 : ∀ (x : E), φ (-x) = φ x
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
have h : D + dist x 0 ≤ 1
Tactic: apply ball_subset_ball'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ D + dist x 0 ≤ 1
have hx₁ : dist x 0 ≤ 1 - D
Tactic: simp only [mem_closedBall] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ D + dist x 0 ≤ 1
have linarith : 1 < D + dist x 0 → 1 - (D + dist x 0) + (dist x 0 - (1 - D)) = 0
Tactic: linarith only [hx]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
have C : 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ φ y = 1
have simp : 1 < dist y 0 → False
Tactic: simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ False
have linarith : dist y 0 - 1 + (1 - dist y 0) = 0
Tactic: linarith only [mem_ball.1 (C hy), h'y]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
have B : ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
have Bx : φ x = 1
Tactic: have Bx : φ x = 1 := B _ (mem_ball_self Dpos)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
have B' : ∀ y ∈ ball x D, φ y = φ x
Tactic: have B' : ∀ y, y ∈ ball x D → φ y = φ x := by rw [Bx]; exact B
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ inst_3 μ fun (t : E) ↦
    (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (w D t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (φ x))
  1
Tactic: rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
⊢ φ y = 0
have simp : ‖y‖ ≤ 1 → False
Tactic: simp only [φ, indicator, mem_closedBall_zero_iff, ite_eq_right_iff, one_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ ball y D ⊆ ball 0 (1 + D)
have h : D + dist y 0 ≤ 1 + D
Tactic: apply ball_subset_ball'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ D + dist y 0 ≤ 1 + D
have h'y₁ : dist y 0 ≤ 1
Tactic: rw [← dist_zero_right] at h'y
Cleared hypotheses: h'y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : dist y 0 ≤ 1
⊢ D + dist y 0 ≤ 1 + D
have linarith : 1 + D < D + dist y 0 → 1 + D - (D + dist y 0) + (dist y 0 - 1) = 0
Tactic: linarith only [h'y]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ False
have C : ball y D ⊆ ball 0 (1 + D)
Tactic: have C : ball y D ⊆ ball 0 (1 + D) := by
      apply ball_subset_ball'
      rw [← dist_zero_right] at h'y
      linarith only [h'y]