awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
h : ∀ (i : ι), (support (M := ℝ) fun (y : G) ↦ (φ i).normed μ (x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
⊢ ∀ᶠ (i : ι) in l,
    Subset.{uG} (α := Set G) (support (M := ℝ) fun (y : G) ↦ (φ i).normed μ (x₀ - y))
      ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i))

Tactic:
filter_upwards with i
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
h : preimage (β := G) (fun (y : G) ↦ x₀ - y) (ball 0 (φ i).rOut) ⊆ closedBall x₀ (φ i).rOut
⊢ support ((φ i).normed μ ∘ fun (y : G) ↦ x₀ - y) ⊆ closedBall x₀ (φ i).rOut

Tactic:
simp only [support_comp_eq_preimage, support_normed_eq]

Premises used: ContDiffBump.support_normed_eq, Function.support_comp_eq_preimage
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
x : G
hx : Membership.mem (γ := Set G) (preimage (β := G) (fun (y : G) ↦ x₀ - y) (ball 0 (φ i).rOut)) x
⊢ ‖x₀ - x‖ < (φ i).rOut

Tactic:
simp only [mem_preimage, mem_ball, dist_zero_right] at hx

Premises used: Metric.mem_ball, dist_zero_right, Set.mem_preimage
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
x : G
hx : ‖x₀ - x‖ < (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut

Tactic:
simpa [dist_eq_norm_sub'] using hx.le

Premises used: LT.lt.le, dist_eq_norm_sub'
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
h :
  ∀ (i : ι) (hi : (φ i).rOut ≤ K * (φ i).rIn) (x : G),
    |(φ i).normed μ (x₀ - x)| ≤ K ^ Module.finrank ℝ G / μ.real (closedBall x₀ (φ i).rOut)
⊢ ∀ᶠ (i : ι) in l,
    ∀ (x : G),
      |(φ i).normed μ (x₀ - x)| ≤
        K ^ Module.finrank ℝ G / μ.real ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i))

Tactic:
filter_upwards [h'φ] with i hi x
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
hi : (φ i).rOut ≤ K * (φ i).rIn
x : G
h : (φ i).normed μ (x₀ - x) ≤ K ^ Module.finrank ℝ G / μ.real (closedBall 0 (φ i).rOut)
⊢ |(φ i).normed μ (x₀ - x)| ≤ K ^ Module.finrank ℝ G / μ.real (closedBall x₀ (φ i).rOut)

Tactic:
rw [abs_of_nonneg (nonneg_normed _ _), addHaar_real_closedBall_center]

Premises used: ContDiffBump.nonneg_normed, MeasureTheory.Measure.addHaar_real_closedBall_center, abs_of_nonneg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
hi : (φ i).rOut ≤ K * (φ i).rIn
x : G
⊢ (φ i).normed μ (x₀ - x) ≤ K ^ Module.finrank ℝ G / μ.real (closedBall 0 (φ i).rOut)

Tactic:
(φ i).normed_le_div_measure_closedBall_rOut _ _ hi _

Premises used: ContDiffBump.normed_le_div_measure_closedBall_rOut
-- Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : NormedSpace ℝ E'
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace ℝ G
inst_5 : CompleteSpace E'
inst_6 : BorelSpace G
inst_7 : FiniteDimensional ℝ G
inst_8 : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump.{uG} (E := G) 0
l : Filter ι
K : ℝ
hφ : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ :
  Tendsto (β := ℝ) (fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ)
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x₀) (𝓝 0)
hφ' : Tendsto (β := ℝ) (fun (i : ι) ↦ (φ i).rOut) l (𝓝[>] 0)
this :
  Tendsto (β := ℝ)
    (Function.comp (β := ℝ) ((fun (a : Set G) ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun (r : ℝ) ↦ closedBall x₀ r)
      fun (i : ι) ↦ (φ i).rOut)
    l (𝓝 0)
i : ι
hi : (φ i).rOut ≤ K * (φ i).rIn
x : G
⊢ (φ i).normed μ (x₀ - x) ≤ K ^ Module.finrank ℝ G / μ.real (closedBall 0 (φ i).rOut)

Tactic:
exact (φ i).normed_le_div_measure_closedBall_rOut _ _ hi _

Premises used: ContDiffBump.normed_le_div_measure_closedBall_rOut
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
obtain :
  ∀ (d : ℝ) (d_pos : 0 < d) (hd : Euclidean.closedBall x d ⊆ s),
    ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Tactic:
obtain ⟨d : ℝ, d_pos : 0 < d, hd : Euclidean.closedBall x d ⊆ s⟩ :=
    Euclidean.nhds_basis_closedBall.mem_iff.1 hs

Premises used: Filter.HasBasis.mem_iff, Euclidean.nhds_basis_closedBall, Iff.mp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
y : E
hy : y ∈ support f
⊢ Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (support (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ))
    (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) y :
      EuclideanSpace ℝ (Fin (finrank ℝ E)))

Tactic:
simpa only [Function.mem_support, Function.comp_apply, Ne] using hy

Premises used: Ne, Function.mem_support, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
y : E
hy : y ∈ support f
⊢ Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (support (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ))
    (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) y :
      EuclideanSpace ℝ (Fin (finrank ℝ E)))

Tactic:
have : toEuclidean y ∈ Function.support c := by
      simpa only [Function.mem_support, Function.comp_apply, Ne] using hy
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
y : E
hy : y ∈ support f
this :
  Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (support (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ))
    (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) y :
      EuclideanSpace ℝ (Fin (finrank ℝ E)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (γ := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
        (ball
            (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) :
                (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
              x)
            c.rOut :
          Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
            y :
          EuclideanSpace ℝ (Fin (finrank ℝ E)))),
    y ∈ Euclidean.ball x d
⊢ y ∈ Euclidean.ball x d

Tactic:
rwa [c.support_eq] at this

Premises used: ContDiffBump.support_eq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
⊢ support f ⊆ Euclidean.ball x d

Tactic:
have f_supp : f.support ⊆ Euclidean.ball x d := by
    intro y hy
    have : toEuclidean y ∈ Function.support c := by
      simpa only [Function.mem_support, Function.comp_apply, Ne] using hy
    rwa [c.support_eq] at this
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
rw :
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support f) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Euclidean.ball x d)
⊢ tsupport f ⊆ Euclidean.closedBall x d

Tactic:
rw [tsupport, ← Euclidean.closure_ball _ d_pos.ne']

Premises used: tsupport, LT.lt.ne', Euclidean.closure_ball
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support f) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Euclidean.ball x d)

Tactic:
closure_mono f_supp

Premises used: closure_mono
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support f) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Euclidean.ball x d)

Tactic:
exact closure_mono f_supp

Premises used: closure_mono
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
⊢ tsupport f ⊆ Euclidean.closedBall x d

Tactic:
have f_tsupp : tsupport f ⊆ Euclidean.closedBall x d := by
    rw [tsupport, ← Euclidean.closure_ball _ d_pos.ne']
    exact closure_mono f_supp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Tactic:
⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
refine_1 : HasCompactSupport f
refine_2 : ContDiff ℝ (↑n : ℕ∞ω) f
refine_3 : range f ⊆ Icc 0 1
refine_4 : f x = 1
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1

Tactic:
refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ HasCompactSupport f

Tactic:
isCompact_of_isClosed_isBounded isClosed_closure ?_

Premises used: Metric.isCompact_of_isClosed_isBounded, isClosed_closure, HasCompactSupport
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
refine_1 : Bornology.IsBounded (tsupport f)
⊢ HasCompactSupport f

Tactic:
refine isCompact_of_isClosed_isBounded isClosed_closure ?_

Premises used: Metric.isCompact_of_isClosed_isBounded, isClosed_closure
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ Bornology.IsBounded (Euclidean.closedBall x d)

Tactic:
have : IsBounded (Euclidean.closedBall x d) := Euclidean.isCompact_closedBall.isBounded