awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
⊢ ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x
have apply : ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x
Tactic: apply ContDiff.of_le _ (show n ≤ ∞ from mod_cast le_top)
-- 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
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
⊢ ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x
have contDiff_tsum_of_eventually : ∀ (k : ℕ),
  LE.le (α := ℕ∞) (↑k : ℕ∞) ⊤ →
    ∀ᶠ (i : ℕ) in Filter.cofinite,
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ E) ℝ) (iteratedFDeriv ℝ k (r i • g i) x) ≤ (↑(δ i) : ℝ)
Tactic: refine
      contDiff_tsum_of_eventually (fun k => (g_smooth k).const_smul (r k))
        (fun k _ => (NNReal.hasSum_coe.2 δc).summable) ?_
-- 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
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
i : ℕ
h : LE.le (α := ℕ∞) (↑i : ℕ∞) ⊤
⊢ ∀ᶠ (i_1 : ℕ) in Filter.cofinite,
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r i_1 • g i_1) x) ≤
        (↑(δ i_1) : ℝ)
have simp : ∃ (a : ℕ),
  ∀ b ≥ a,
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r b • g b) x) ≤ (↑(δ b) : ℝ)
Tactic: simp only [Nat.cofinite_eq_atTop, Filter.eventually_atTop]
-- 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
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y)
have inr : (fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y ≤ (↑c : ℝ)
Tactic: refine ⟨tsum_nonneg fun n => mul_nonneg (rpos n).le (g_nonneg n y), le_trans ?_ c_lt.le⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
⊢ (fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y ≤ (↑c : ℝ)
have A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
Tactic: have A : HasSum (fun n => (δ n : ℝ)) c := NNReal.hasSum_coe.2 δc
-- 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
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
⊢ (fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y ≤ (↑c : ℝ)
have inr : LE.le (α := ℝ) (∑' (n : ℕ), r n * g n y) (∑' (b : ℕ), (↑(δ b) : ℝ))
Tactic: simp only [Pi.smul_apply, smul_eq_mul, NNReal.val_eq_coe, ← A.tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
⊢ LE.le (α := ℝ) (∑' (n : ℕ), r n * g n y) (∑' (b : ℕ), (↑(δ b) : ℝ))
have apply : ∀ (i : ℕ), (r i • g i) y ≤ (↑(δ i) : ℝ)
Tactic: apply Summable.tsum_le_tsum _ (S y) A.summable
-- 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_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
n : ℕ
⊢ (r n • g n) y ≤ (↑(δ n) : ℝ)
have apply : |(r n • g n) y| ≤ (↑(δ n) : ℝ)
Tactic: apply (le_abs_self _).trans
-- 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
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
Tactic: have A : IsOpen (ball (0 : E) 1) := isOpen_ball
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have obtain : ∀ (f : E → ℝ) (f_support : support f = ball 0 1) (f_smooth : ContDiff ℝ ∞ f) (f_range : range f ⊆ Icc 0 1),
  ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
Tactic: obtain ⟨f, f_support, f_smooth, f_range⟩ :
      ∃ f : E → ℝ, f.support = ball (0 : E) 1 ∧ ContDiff ℝ ∞ f ∧ Set.range f ⊆ Set.Icc 0 1 :=
    A.exists_contDiff_support_eq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
Tactic: have B : ∀ x, f x ∈ Icc (0 : ℝ) 1 := fun x => f_range (mem_range_self x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have refine_1 : ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2
Tactic: refine ⟨fun x => (f x + f (-x)) / 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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
refine_1 : ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have refine_2 : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)
Tactic: refine ⟨fun x => (f x + f (-x)) / 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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
refine_1 : ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2
refine_2 : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have refine_3 : Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)
Tactic: refine ⟨fun x => (f x + f (-x)) / 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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
refine_1 : ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2
refine_2 : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)
refine_3 : Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
have refine_4 : ∀ (x : E), Eq (α := ℝ) ((fun (x : E) ↦ (f x + f (-x)) / 2) (-x)) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)
Tactic: refine ⟨fun x => (f x + f (-x)) / 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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
⊢ 0 ≤ (f x + f (-x)) / 2 ∧ (f x + f (-x)) / 2 ≤ 1
have refine_2 : 0 ≤ (f x + f (-x)) / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
refine_2 : 0 ≤ (f x + f (-x)) / 2
⊢ 0 ≤ (f x + f (-x)) / 2 ∧ (f x + f (-x)) / 2 ≤ 1
have refine_2₁ : (f x + f (-x)) / 2 ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
⊢ 0 ≤ (f x + f (-x)) / 2
have linarith : (f x + f (-x)) / 2 < 0 → 2 / 2 = 1
Tactic: linarith [(B x).1, (B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : (f x + f (-x)) / 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ (f x + f (-x)) / 2
have linarith₁ : (f x + f (-x)) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(B x).1, (B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : (f x + f (-x)) / 2 < 0 → 2 / 2 = 1
linarith₁ : (f x + f (-x)) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ (f x + f (-x)) / 2
have linarith₂ : (f x + f (-x)) / 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [(B x).1, (B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : (f x + f (-x)) / 2 < 0 → 2 / 2 = 1
linarith₁ : (f x + f (-x)) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (f x + f (-x)) / 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ (f x + f (-x)) / 2
have linarith₃ : (f x + f (-x)) / 2 < 0 → 1 * f x + 1 * f (-x) - HMul.hMul (α := ℝ) 2 0 + (0 - f x) + (0 - f (-x)) = 0
Tactic: linarith [(B x).1, (B (-x)).1]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
⊢ (f x + f (-x)) / 2 ≤ 1
have linarith : 1 < (f x + f (-x)) / 2 → 2 / 2 = 1
Tactic: linarith [(B x).2, (B (-x)).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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : 1 < (f x + f (-x)) / 2 → 2 / 2 = 1
⊢ (f x + f (-x)) / 2 ≤ 1
have linarith₁ : 1 < (f x + f (-x)) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [(B x).2, (B (-x)).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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : 1 < (f x + f (-x)) / 2 → 2 / 2 = 1
linarith₁ : 1 < (f x + f (-x)) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (f x + f (-x)) / 2 ≤ 1
have linarith₂ : 1 < (f x + f (-x)) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith [(B x).2, (B (-x)).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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : 1 < (f x + f (-x)) / 2 → 2 / 2 = 1
linarith₁ : 1 < (f x + f (-x)) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < (f x + f (-x)) / 2 → GT.gt (α := ℝ) 2 0
⊢ (f x + f (-x)) / 2 ≤ 1
have linarith₃ : 1 < (f x + f (-x)) / 2 → HMul.hMul (α := ℝ) 2 1 - (1 * f x + 1 * f (-x)) + (f x - 1) + (f (-x) - 1) = 0
Tactic: linarith [(B x).2, (B (-x)).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
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)
have refine_3 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 1) x), (f x + f (-x)) / 2 ≠ 0
Tactic: refine support_eq_iff.2 ⟨fun x hx => ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
refine_3 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 1) x), (f x + f (-x)) / 2 ≠ 0
⊢ Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)
have refine_3₁ : ∀ (x : E) (hx : x ∉ ball 0 1), (f x + f (-x)) / 2 = 0
Tactic: refine support_eq_iff.2 ⟨fun x hx => ?_, fun x hx => ?_⟩