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
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
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_3 μ fun (t : E) ↦
      (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (w D t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (φ x))
    1

Tactic:
simp only [lsmul_apply, smul_eq_mul, integral_mul_const, w_integral E Dpos, Bx,
    one_mul]

Premises used: ContinuousLinearMap.lsmul_apply, smul_eq_mul, ExistsContDiffBumpBase.w_integral, one_mul, MeasureTheory.integral_mul_const
-- 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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
simp : ‖y‖ ≤ 1 → False
⊢ φ y = 0

Tactic:
simp only [φ, indicator, mem_closedBall_zero_iff, ite_eq_right_iff, one_ne_zero]

Premises used: Set.indicator, ite_eq_right_iff, ExistsContDiffBumpBase.φ, mem_closedBall_zero_iff, one_ne_zero
-- 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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
h : D + dist y 0 ≤ 1 + D
⊢ ball y D ⊆ ball 0 (1 + D)

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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ dist y 0 ≤ 1

Tactic:
rw [← dist_zero_right] at h'y

Premises used: 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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : dist y 0 ≤ 1
linarith : 1 + D < D + dist y 0 → 1 + D - (D + dist y 0) + (dist y 0 - 1) = 0
⊢ D + dist y 0 ≤ 1 + D

Tactic:
linarith only [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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ 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]
-- 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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
C : ball y D ⊆ ball 0 (1 + D)
⊢ False

Tactic:
hx (C (mem_ball_comm.1 hy))

Premises used: Iff.mp, Metric.mem_ball_comm
-- 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 : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
C : ball y D ⊆ ball 0 (1 + D)
⊢ False

Tactic:
exact hx (C (mem_ball_comm.1 hy))

Premises used: Iff.mp, Metric.mem_ball_comm
-- 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 : x ∉ ball 0 (1 + D)
⊢ ∀ y ∈ ball x D, φ y = 0

Tactic:
have B : ∀ y, y ∈ ball x D → φ y = 0 := by
    intro y hy
    simp only [φ, indicator, mem_closedBall_zero_iff, ite_eq_right_iff, one_ne_zero]
    intro h'y
    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]
    exact hx (C (mem_ball_comm.1 hy))
-- 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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
⊢ φ x = 0

Tactic:
have Bx : φ x = 0 := 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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
rw : ∀ y ∈ ball x D, φ y = 0
⊢ ∀ 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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
⊢ ∀ y ∈ ball x D, φ y = 0

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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
⊢ ∀ y ∈ ball x D, φ y = 0

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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
⊢ ∀ 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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
B' : ∀ y ∈ ball x D, φ y = φ x
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ inst_3 μ fun (t : E) ↦
      (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (w D t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (φ x))
    0
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0

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
-- 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 : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_3 μ fun (t : E) ↦
      (((lsmul ℝ ℝ : (a : ℝ) → ℝ →L[ℝ] ℝ) (w D t) : ℝ →L[ℝ] ℝ) : (a : ℝ) → ℝ) (φ x))
    0

Tactic:
simp only [lsmul_apply, smul_eq_mul, Bx, mul_zero, integral_const]

Premises used: ContinuousLinearMap.lsmul_apply, MulZeroClass.mul_zero, MeasureTheory.integral_const, 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
⊢ 0 ≤ y D x

Tactic:
integral_nonneg (w_mul_φ_nonneg D x)

Premises used: MeasureTheory.integral_nonneg, ExistsContDiffBumpBase.y, MeasureTheory.convolution, ExistsContDiffBumpBase.w_mul_φ_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
Dpos : 0 < D
convolution_mono_right_of_nonneg : ConvolutionExistsAt (E' := ℝ) (w D) (fun (x : E) ↦ 1) x (lsmul ℝ ℝ) μ
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x

Tactic:
apply
      convolution_mono_right_of_nonneg _ (w_nonneg D) (indicator_le_self' fun x _ => zero_le_one)
        fun _ => zero_le_one

Premises used: Set.indicator_le_self', MeasureTheory.convolution_mono_right_of_nonneg, zero_le_one, ExistsContDiffBumpBase.w_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
Dpos : 0 < D
⊢ ConvolutionExistsAt (E' := ℝ) (w D) (fun (x : E) ↦ 1) x (lsmul ℝ ℝ) μ

Tactic:
((w_compact_support E Dpos).convolutionExists_left _ ?_
      (locallyIntegrable_const (1 : ℝ)) x).integrable

Premises used: MeasureTheory.ConvolutionExistsAt.integrable, ExistsContDiffBumpBase.w_compact_support, MeasureTheory.ConvolutionExistsAt, MeasureTheory.locallyIntegrable_const, HasCompactSupport.convolutionExists_left, 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 : ℝ
x : E
Dpos : 0 < D
refine : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (w D)
⊢ ConvolutionExistsAt (E' := ℝ) (w D) (fun (x : E) ↦ 1) x (lsmul ℝ ℝ) μ

Tactic:
refine ((w_compact_support E Dpos).convolutionExists_left _ ?_
      (locallyIntegrable_const (1 : ℝ)) x).integrable

Premises used: MeasureTheory.ConvolutionExistsAt.integrable, ExistsContDiffBumpBase.w_compact_support, MeasureTheory.locallyIntegrable_const, HasCompactSupport.convolutionExists_left, 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 : ℝ
x : E
Dpos : 0 < D
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (HSMul.hSMul D⁻¹)

Tactic:
fun_prop
-- 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
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (w D)

Tactic:
exact continuous_const.mul ((u_continuous E).comp (by fun_prop))

Premises used: ExistsContDiffBumpBase.u_continuous, Continuous.comp, continuous_const, Continuous.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
Dpos : 0 < D
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x

Tactic:
have A : (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x := by
    apply
      convolution_mono_right_of_nonneg _ (w_nonneg D) (indicator_le_self' fun x _ => zero_le_one)
        fun _ => zero_le_one
    refine ((w_compact_support E Dpos).convolutionExists_left _ ?_
      (locallyIntegrable_const (1 : ℝ)) x).integrable
    exact continuous_const.mul ((u_continuous E).comp (by fun_prop))
-- 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
A : (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x
⊢ Eq (α := ℝ) ((w D ⋆[lsmul ℝ ℝ, μ] fun (x : E) ↦ 1) x) 1

Tactic:
simp only [convolution, mul_one, lsmul_apply, smul_eq_mul, w_integral E Dpos]

Premises used: ContinuousLinearMap.lsmul_apply, MeasureTheory.convolution, smul_eq_mul, ExistsContDiffBumpBase.w_integral, mul_one
-- 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
A : (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x
⊢ Eq (α := ℝ) ((w D ⋆[lsmul ℝ ℝ, μ] fun (x : E) ↦ 1) x) 1

Tactic:
have B : (w D ⋆[lsmul ℝ ℝ, μ] fun _ => (1 : ℝ)) x = 1 := by
    simp only [convolution, mul_one, lsmul_apply, smul_eq_mul, w_integral E 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
A : (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x
B : Eq (α := ℝ) ((w D ⋆[lsmul ℝ ℝ, μ] fun (x : E) ↦ 1) x) 1
⊢ y D x ≤ 1

Tactic:
A.trans (le_of_eq B)

Premises used: ExistsContDiffBumpBase.y, LE.le.trans, le_of_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
Dpos : 0 < D
A : (w D ⋆[lsmul ℝ ℝ, μ] φ) x ≤ (w D ⋆[lsmul ℝ ℝ, μ] 1) x
B : Eq (α := ℝ) ((w D ⋆[lsmul ℝ ℝ, μ] fun (x : E) ↦ 1) x) 1
⊢ y D x ≤ 1

Tactic:
exact A.trans (le_of_eq B)

Premises used: LE.le.trans, le_of_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
Dpos : 0 < D
D_lt_one : D < 1
hx : Membership.mem (γ := Set E) (ball 0 (1 + D)) x
⊢ ‖x‖ < 1 + D

Tactic:
simp only [mem_ball_zero_iff] at hx

Premises used: mem_ball_zero_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 : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ 0 < y D x

Tactic:
(integral_pos_iff_support_of_nonneg (w_mul_φ_nonneg D x) ?_).2 ?_

Premises used: Iff.mpr, ExistsContDiffBumpBase.y, MeasureTheory.integral_pos_iff_support_of_nonneg, MeasureTheory.convolution, ExistsContDiffBumpBase.w_mul_φ_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
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
refine_1 : @Integrable ℝ _ _ _ inst_3 (fun (i : E) ↦ w D i * φ (x - i)) μ
refine_2 :
  LT.lt (α := ENNReal) (0 : ENNReal)
    (((μ : Measure E) : (a : Set E) → ENNReal) (support (M := ℝ) fun (i : E) ↦ w D i * φ (x - i)) : ENNReal)
⊢ 0 < y D x

Tactic:
refine (integral_pos_iff_support_of_nonneg (w_mul_φ_nonneg D x) ?_).2 ?_

Premises used: Iff.mpr, MeasureTheory.integral_pos_iff_support_of_nonneg, ExistsContDiffBumpBase.w_mul_φ_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
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ HasCompactSupport.{u_1, 0} (α := E) (w D)

Tactic:
have F_comp : HasCompactSupport (w D) := w_compact_support E 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport.{u_1, 0} (α := E) (w D)
⊢ LocallyIntegrable.{u_1, 0} (X := E) φ μ

Tactic:
have B : LocallyIntegrable (φ : E → ℝ) μ :=
      (locallyIntegrable_const _).indicator measurableSet_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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport.{u_1, 0} (α := E) (w D)
B : LocallyIntegrable.{u_1, 0} (X := E) φ μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (HSMul.hSMul D⁻¹)

Tactic:
fun_prop
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport.{u_1, 0} (α := E) (w D)
B : LocallyIntegrable.{u_1, 0} (X := E) φ μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (w D)

Tactic:
have C : Continuous (w D : E → ℝ) :=
      continuous_const.mul ((u_continuous E).comp (by fun_prop))
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport.{u_1, 0} (α := E) (w D)
B : LocallyIntegrable.{u_1, 0} (X := E) φ μ
C : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (w D)
⊢ @Integrable ℝ _ _ _ inst_3 (fun (i : E) ↦ w D i * φ (x - i)) μ

Tactic:
(F_comp.convolutionExists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) C B x).integrable

Premises used: Real, MeasureTheory.ConvolutionExistsAt.integrable, HasCompactSupport.convolutionExists_left, ContinuousLinearMap.lsmul
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport.{u_1, 0} (α := E) (w D)
B : LocallyIntegrable.{u_1, 0} (X := E) φ μ
C : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (w D)
⊢ @Integrable ℝ _ _ _ inst_3 (fun (i : E) ↦ w D i * φ (x - i)) μ

Tactic:
exact (F_comp.convolutionExists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) C B x).integrable

Premises used: Real, MeasureTheory.ConvolutionExistsAt.integrable, HasCompactSupport.convolutionExists_left, ContinuousLinearMap.lsmul
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ let z := (D / (1 + D)) • x;
  z = (D / (1 + D)) • x

Tactic:
set z := (D / (1 + D)) • x with hz

Premises used: HDiv.hDiv, HAdd.hAdd, 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 : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
linarith : 1 + D ≤ 0 → 2 * (0 - D) + (D - 1) + (1 + D - 0) = 0
linarith₁ : 1 + D ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 + D

Tactic:
linarith
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
⊢ 0 < 1 + D

Tactic:
have B : 0 < 1 + D := by linarith
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
simp : Membership.mem (γ := Set E) (ball 0 D ∩ support (M := ℝ) fun (x_1 : E) ↦ φ (x - x_1)) y
⊢ Membership.mem (γ := Set E) (support (M := ℝ) fun (y : E) ↦ w D y * φ (x - y)) y

Tactic:
simp only [support_mul, w_support E Dpos]

Premises used: ExistsContDiffBumpBase.w_support, Function.support_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
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
simp : Membership.mem (γ := Set E) (ball 0 D) y ∧ ‖x - y‖ ≤ 1
⊢ Membership.mem (γ := Set E) (ball 0 D ∩ support (M := ℝ) fun (x_1 : E) ↦ φ (x - x_1)) y

Tactic:
simp only [φ, mem_inter_iff, mem_support, Ne, indicator_apply_eq_zero,
        mem_closedBall_zero_iff, one_ne_zero, not_forall, not_false_iff, exists_prop, and_true]

Premises used: and_true, Set.mem_inter_iff, Ne, exists_prop, Function.mem_support, ExistsContDiffBumpBase.φ, mem_closedBall_zero_iff, not_false_iff, one_ne_zero, Set.indicator_apply_eq_zero, Classical.not_forall
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
left : Membership.mem (γ := Set E) (ball 0 D) y
right : ‖x - y‖ ≤ 1
⊢ Membership.mem (γ := Set E) (ball 0 D) y ∧ ‖x - y‖ ≤ 1

Tactic:
constructor
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
apply : D * (1 + D - ‖x‖) / (1 + D) + dist z 0 ≤ D
⊢ Membership.mem (γ := Set E) (ball 0 D) y

Tactic:
apply ball_subset_ball' _ hy

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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
simp : D * (1 + D - ‖x‖) / (1 + D) + D / (1 + D) * ‖x‖ ≤ D
⊢ D * (1 + D - ‖x‖) / (1 + D) + dist z 0 ≤ D

Tactic:
simp only [hz, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right,
          Real.norm_eq_abs, abs_div]

Premises used: norm_smul, abs_div, LT.lt.le, abs_of_nonneg, dist_zero_right, Real.norm_eq_abs
-- 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
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
field_simp : 1 + D - ‖x‖ + ‖x‖ ≤ 1 + D
⊢ D * (1 + D - ‖x‖) / (1 + D) + D / (1 + D) * ‖x‖ ≤ D

Tactic:
field_simp