awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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 : ι) 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))
have h : ∀ (i : ι), (support (M := ℝ) fun (y : G) ↦ (φ i).normed μ (x₀ - y)) ⊆ closedBall x₀ (φ i).rOut
Tactic: filter_upwards with i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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 : ι
⊢ support ((φ i).normed μ ∘ fun (y : G) ↦ x₀ - y) ⊆ closedBall x₀ (φ i).rOut
have h : preimage (β := G) (fun (y : G) ↦ x₀ - y) (ball 0 (φ i).rOut) ⊆ closedBall x₀ (φ i).rOut
Tactic: simp only [support_comp_eq_preimage, support_normed_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (hypothesis)
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 ∈ closedBall x₀ (φ i).rOut
have hx₁ : ‖x₀ - x‖ < (φ i).rOut
Tactic: simp only [mem_preimage, mem_ball, dist_zero_right] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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 : ι) in l,
    ∀ (x : G),
      |(φ i).normed μ (x₀ - x)| ≤
        K ^ Module.finrank ℝ G / μ.real ((fun (r : ℝ) ↦ closedBall x₀ r) ((fun (i : ι) ↦ (φ i).rOut) i))
have h : ∀ (i : ι) (hi : (φ i).rOut ≤ K * (φ i).rIn) (x : G),
  |(φ i).normed μ (x₀ - x)| ≤ K ^ Module.finrank ℝ G / μ.real (closedBall x₀ (φ i).rOut)
Tactic: filter_upwards [h'φ] with i hi x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.Convolution (goal)
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 x₀ (φ i).rOut)
have h : (φ i).normed μ (x₀ - x) ≤ K ^ Module.finrank ℝ G / μ.real (closedBall 0 (φ i).rOut)
Tactic: rw [abs_of_nonneg (nonneg_normed _ _), addHaar_real_closedBall_center]
-- 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
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
have 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
Tactic: obtain ⟨d : ℝ, d_pos : 0 < d, hd : Euclidean.closedBall x d ⊆ s⟩ :=
    Euclidean.nhds_basis_closedBall.mem_iff.1 hs
-- 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
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
⊢ y ∈ Euclidean.ball x d
have 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)))
Tactic: have : toEuclidean y ∈ Function.support c := by
      simpa only [Function.mem_support, Function.comp_apply, Ne] using hy
-- 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
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)))
⊢ y ∈ Euclidean.ball x d
have 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
Tactic: rwa [c.support_eq] at this
Cleared hypotheses: this
-- 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
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 : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
have f_supp : 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
-- 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
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
have rw : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support f) ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Euclidean.ball x d)
Tactic: rw [tsupport, ← Euclidean.closure_ball _ d_pos.ne']
-- 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
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 : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
have f_tsupp : 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
-- 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
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
have refine_1 : HasCompactSupport f
Tactic: refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩
-- 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
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
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
have refine_2 : ContDiff ℝ (↑n : ℕ∞ω) f
Tactic: refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩
-- 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
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
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
have refine_3 : range f ⊆ Icc 0 1
Tactic: refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩
-- 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
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
⊢ ∃ (f : E → ℝ), tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
have refine_4 : f x = 1
Tactic: refine ⟨f, f_tsupp.trans hd, ?_, ?_, ?_, ?_⟩
-- 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
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
have refine_1 : Bornology.IsBounded (tsupport f)
Tactic: refine isCompact_of_isClosed_isBounded isClosed_closure ?_
-- 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
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 (tsupport f)
have this : Bornology.IsBounded (Euclidean.closedBall x d)
Tactic: have : IsBounded (Euclidean.closedBall x d) := Euclidean.isCompact_closedBall.isBounded
-- 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
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
this : Bornology.IsBounded (Euclidean.closedBall x d)
⊢ Bornology.IsBounded (tsupport f)
have refine_1 : support f ⊆ Euclidean.closedBall x d
Tactic: refine this.subset (Euclidean.isClosed_closedBall.closure_subset_iff.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
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
⊢ ContDiff ℝ (↑n : ℕ∞ω) f
have refine_2 : ContDiff.{0, u_1, 0} ℝ (E := E) (F := EuclideanSpace ℝ (Fin (finrank ℝ E))) (↑n : ℕ∞ω)
  (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
Tactic: apply c.contDiff.comp
-- 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
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 x = 1
have refine_4 : Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (γ := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
  (closedBall
      (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
        x)
      c.rIn :
    Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E)))
Tactic: apply c.one_of_mem_closedBall
-- 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
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
⊢ Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (γ := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (closedBall
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        c.rIn :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
      EuclideanSpace ℝ (Fin (finrank ℝ E)))
have refine_4 : 0 ≤ c.rIn
Tactic: apply mem_closedBall_self
-- 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
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have inl : ∀ (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
  ∃ (f : E → ℝ), support f = ∅ ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
Tactic: rcases eq_empty_or_nonempty s with (rfl | h's)
Cleared hypotheses: s, hs