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
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))
linarith : 1 + D < 1 + D - ‖x‖ + ‖x‖ → 1 + D - (1 + D - ‖x‖ + ‖x‖) = 0
⊢ 1 + D - ‖x‖ + ‖x‖ ≤ 1 + D

Tactic:
linarith only
-- 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))
rw : -(D / (1 + D) - 1) = 1 / (1 + D)
rw₁ : D / (1 + D) - 1 ≤ 0
⊢ ‖D / (1 + D) - 1‖ = 1 / (1 + D)

Tactic:
rw [Real.norm_of_nonpos]

Premises used: Real.norm_of_nonpos
-- 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))
⊢ -(D / (1 + D) - 1) = 1 / (1 + D)

Tactic:
field
-- 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 : D - (1 + D) ≤ (1 + D) * 0
⊢ D / (1 + D) - 1 ≤ 0

Tactic:
field_simp
-- 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))
linarith : (1 + D) * 0 < D - (1 + D) → -1 + ((1 + D) * 0 - (D - (1 + D))) = 0
⊢ D - (1 + D) ≤ (1 + D) * 0

Tactic:
linarith only
-- 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))
⊢ ‖D / (1 + D) - 1‖ = 1 / (1 + D)

Tactic:
have ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D) := by
          rw [Real.norm_of_nonpos]
          · field
          · field_simp
            linarith only
-- 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))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
right : y ∈ closedBall x 1
⊢ ‖x - y‖ ≤ 1

Tactic:
rw [← mem_closedBall_iff_norm']

Premises used: mem_closedBall_iff_norm'
-- 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))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
apply : D * (1 + D - ‖x‖) / (1 + D) + dist z x ≤ 1
⊢ y ∈ closedBall x 1

Tactic:
apply closedBall_subset_closedBall' _ (ball_subset_closedBall hy)

Premises used: Metric.ball_subset_closedBall, Metric.closedBall_subset_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
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))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
rw : D * (1 + D - ‖x‖) / (1 + D) + 1 / (1 + D) * ‖x‖ ≤ 1
⊢ D * (1 + D - ‖x‖) / (1 + D) + dist z x ≤ 1

Tactic:
rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID]

Premises used: Real, dist_eq_norm, norm_smul, sub_smul, one_smul
-- 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))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
field_simp : D * (1 + D - ‖x‖) + ‖x‖ ≤ 1 + D
⊢ D * (1 + D - ‖x‖) / (1 + D) + 1 / (1 + D) * ‖x‖ ≤ 1

Tactic:
field_simp
-- 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))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
nlinarith : 1 + D < D * (1 + D - ‖x‖) + ‖x‖ → 1 + D - (D * (1 + D - ‖x‖) + ‖x‖) + (0 - (‖x‖ - (1 + D)) * (D - 1)) = 0
⊢ D * (1 + D - ‖x‖) + ‖x‖ ≤ 1 + D

Tactic:
nlinarith only [hx, D_lt_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
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
⊢ ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support (M := ℝ) fun (y : E) ↦ w D y * φ (x - y)

Tactic:
have C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support fun y : E => w D y * φ (x - y) := by
      intro y hy
      simp only [support_mul, w_support E Dpos]
      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]
      constructor
      · apply ball_subset_ball' _ hy
        simp only [hz, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right,
          Real.norm_eq_abs, abs_div]
        field_simp
        linarith only
      · have ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D) := by
          rw [Real.norm_of_nonpos]
          · field
          · field_simp
            linarith only
        rw [← mem_closedBall_iff_norm']
        apply closedBall_subset_closedBall' _ (ball_subset_closedBall hy)
        rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID]
        field_simp
        nlinarith only [hx, D_lt_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
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
C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support (M := ℝ) fun (y : E) ↦ w D y * φ (x - y)
apply :
  LT.lt (α := ENNReal) (0 : ENNReal)
    (((μ : Measure E) : (a : Set E) → ENNReal) (ball z (D * (1 + D - ‖x‖) / (1 + D))) : ENNReal)
⊢ LT.lt (α := ENNReal) (0 : ENNReal)
    (((μ : Measure E) : (a : Set E) → ENNReal) (support (M := ℝ) fun (i : E) ↦ w D i * φ (x - i)) : ENNReal)

Tactic:
apply lt_of_lt_of_le _ (measure_mono C)

Premises used: MeasureTheory.measure_mono, lt_of_lt_of_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
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
C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support (M := ℝ) fun (y : E) ↦ w D y * φ (x - y)
hr : 0 < D * (1 + D - ‖x‖) / (1 + D)
⊢ LT.lt (α := ENNReal) (0 : ENNReal)
    (((μ : Measure E) : (a : Set E) → ENNReal) (ball z (D * (1 + D - ‖x‖) / (1 + D))) : ENNReal)

Tactic:
apply measure_ball_pos

Premises used: 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 : ℝ
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
C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support (M := ℝ) fun (y : E) ↦ w D y * φ (x - y)
linarith : 1 + D - ‖x‖ ≤ 0 → 1 + D - ‖x‖ - 0 + (‖x‖ - (1 + D)) = 0
⊢ 0 < 1 + D - ‖x‖

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
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
C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support (M := ℝ) fun (y : E) ↦ w D y * φ (x - y)
⊢ 0 < D * (1 + D - ‖x‖) / (1 + D)

Tactic:
exact div_pos (mul_pos Dpos (by linarith only [hx])) B

Premises used: mul_pos, div_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
⊢ IsOpen (X := ℝ) (Ioo 0 1)

Tactic:
have hs : IsOpen (Ioo (0 : ℝ) (1 : ℝ)) := isOpen_Ioo
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
⊢ IsCompact.{u_1} (X := E) (closedBall 0 1)

Tactic:
have hk : IsCompact (closedBall (0 : E) 1) := 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_

Premises used: MeasureTheory.contDiffOn_convolution_left_with_param, Real, ExistsContDiffBumpBase.y, MeasureTheory.convolution, 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_1 : ∀ (p : ℝ) (x : E), Membership.mem (γ := Set ℝ) (Ioo 0 1) p → x ∉ closedBall 0 1 → w p x = 0
refine_2 : LocallyIntegrable.{u_1, 0} (X := E) φ μ
refine_3 : ContDiffOn ℝ ∞ (HasUncurry.uncurry (α := ℝ → E → ℝ) w) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ ∞ (uncurry y) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
refine contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_

Premises used: MeasureTheory.contDiffOn_convolution_left_with_param, Real, 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : x ∉ closedBall 0 1
refine_1 : (|p| ^ finrank ℝ E = 0 ∨ Eq (α := ℝ) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) 0) ∨ u (p⁻¹ • x) = 0
⊢ w p x = 0

Tactic:
simp only [w, mul_inv_rev, smul_eq_mul, mul_eq_zero, inv_eq_zero]

Premises used: inv_eq_zero, mul_eq_zero, ExistsContDiffBumpBase.w, 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : x ∉ closedBall 0 1
refine_1 : u (p⁻¹ • x) = 0
⊢ (|p| ^ finrank ℝ E = 0 ∨ Eq (α := ℝ) (@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) 0) ∨ u (p⁻¹ • x) = 0

Tactic:
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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : x ∉ closedBall 0 1
refine_1 : ∀ (hx : u (p⁻¹ • x) ≠ 0), Membership.mem (γ := Set E) (closedBall 0 1) x
⊢ u (p⁻¹ • x) = 0

Tactic:
contrapose! 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
⊢ Membership.mem (γ := Set E) (support u) (p⁻¹ • x)

Tactic:
have : p⁻¹ • x ∈ support u := mem_support.2 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
this : Membership.mem (γ := Set E) (support u) (p⁻¹ • x)
⊢ ‖x‖ < p

Tactic:
simp only [u_support, norm_smul, mem_ball_zero_iff, Real.norm_eq_abs, abs_inv,
      abs_of_nonneg hp.1.le, ← div_eq_inv_mul, div_lt_one hp.1] at this

Premises used: ExistsContDiffBumpBase.u_support, norm_smul, abs_inv, LT.lt.le, And.left, div_lt_one, abs_of_nonneg, div_eq_inv_mul, Real.norm_eq_abs, 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
this : ‖x‖ < p
refine_1 : ‖x‖ ≤ 1
⊢ Membership.mem (γ := Set E) (closedBall 0 1) x

Tactic:
rw [mem_closedBall_zero_iff]

Premises used: mem_closedBall_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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
this : ‖x‖ < p
⊢ ‖x‖ ≤ 1

Tactic:
this.le.trans hp.2.le

Premises used: LT.lt.le, And.right, LE.le.trans
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
p : ℝ
x : E
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
hx : u (p⁻¹ • x) ≠ 0
this : ‖x‖ < p
⊢ ‖x‖ ≤ 1

Tactic:
exact this.le.trans hp.2.le

Premises used: LT.lt.le, And.right, LE.le.trans
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ LocallyIntegrable.{u_1, 0} (X := E) φ μ

Tactic:
(locallyIntegrable_const _).indicator measurableSet_closedBall

Premises used: MeasureTheory.LocallyIntegrable.indicator, ExistsContDiffBumpBase.φ, 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ LocallyIntegrable.{u_1, 0} (X := E) φ μ

Tactic:
exact (locallyIntegrable_const _).indicator measurableSet_closedBall

Premises used: MeasureTheory.LocallyIntegrable.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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |x.1| ^ finrank ℝ E)⁻¹)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
refine_3₁ :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ u (x.1⁻¹ • x.2)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ ∞ (HasUncurry.uncurry (α := ℝ → E → ℝ) w) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
apply ContDiffOn.mul

Premises used: ContDiffOn.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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |x.1| ^ finrank ℝ E)⁻¹)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
(contDiffOn_const.mul ?_).inv fun x hx =>
          ne_of_gt (mul_pos (u_int_pos E) (pow_pos (abs_pos_of_pos hx.1.1) (finrank ℝ E)))

Premises used: pow_pos, Real, abs_pos_of_pos, ne_of_gt, ExistsContDiffBumpBase.u_int_pos, mul_pos, And.left, ContDiffOn.inv, ContDiffOn.mul, Module.finrank, contDiffOn_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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 :
  ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ |x.1| ^ finrank ℝ E) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ ((@integral _ _ _ _ inst_3 μ fun (x : E) ↦ u x) * |x.1| ^ finrank ℝ E)⁻¹)
    (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
refine
        (contDiffOn_const.mul ?_).inv fun x hx =>
          ne_of_gt (mul_pos (u_int_pos E) (pow_pos (abs_pos_of_pos hx.1.1) (finrank ℝ E)))

Premises used: pow_pos, Real, ne_of_gt, ExistsContDiffBumpBase.u_int_pos, mul_pos, ContDiffOn.inv, ContDiffOn.mul, Module.finrank, contDiffOn_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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 : ContDiffOn ℝ (F := ℝ) ∞ (fun (y : ℝ × E) ↦ |y.1|) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ |x.1| ^ finrank ℝ E) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
apply ContDiffOn.pow

Premises used: ContDiffOn.pow
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 : ContDiffOn ℝ ∞ Prod.fst (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
refine_3₁ : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ, x.1 ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (y : ℝ × E) ↦ ‖y.1‖) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
apply ContDiffOn.norm ℝ

Premises used: Real, ContDiffOn.norm
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ Prod.fst (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
contDiffOn_fst

Premises used: contDiffOn_fst
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ Prod.fst (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
exact contDiffOn_fst

Premises used: contDiffOn_fst
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
x : ℝ × E
hx : x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ
⊢ x.1 ≠ 0

Tactic:
ne_of_gt hx.1.1

Premises used: ne_of_gt, And.left
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
x : ℝ × E
hx : x ∈ SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ
⊢ x.1 ≠ 0

Tactic:
exact ne_of_gt hx.1.1

Premises used: ne_of_gt, And.left
-- 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
hs : IsOpen (X := ℝ) (Ioo 0 1)
hk : IsCompact.{u_1} (X := E) (closedBall 0 1)
refine_3 :
  ContDiffOn ℝ (F := E) ∞ (fun (x : ℝ × E) ↦ x.1⁻¹ • x.2) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)
⊢ ContDiffOn ℝ (F := ℝ) ∞ (fun (x : ℝ × E) ↦ u (x.1⁻¹ • x.2)) (SProd.sprod (α := Set ℝ) (β := Set E) (Ioo 0 1) univ)

Tactic:
apply (u_smooth E).comp_contDiffOn

Premises used: ContDiff.comp_contDiffOn, ExistsContDiffBumpBase.u_smooth