awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
n : ℕ
⊢ ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
have this : ∀ (i : ℕ),
  ∃ (R : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R
Tactic: have : ∀ i, ∃ R, ∀ x, ‖iteratedFDeriv ℝ i (fun x => g n x) x‖ ≤ R := by
      intro i
      have : BddAbove (range fun x => ‖iteratedFDeriv ℝ i (fun x : E => g n x) x‖) := by
        apply ((g_smooth n).continuous_iteratedFDeriv
          (mod_cast le_top)).norm.bddAbove_range_of_hasCompactSupport
        apply HasCompactSupport.comp_left _ norm_zero
        apply (g_comp_supp n).iteratedFDeriv
      rcases this with ⟨R, hR⟩
      exact ⟨R, fun x => hR (mem_range_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_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
n : ℕ
this :
  ∀ (i : ℕ),
    ∃ (R : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R
⊢ ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
have choose : ∀ (R : (i : ℕ) → ℝ)
  (hR :
    ∀ (i : ℕ) (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤
        R i),
  ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
Tactic: choose R hR using 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
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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
⊢ ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
have δnpos : 0 < δ n
Tactic: have δnpos : 0 < δ n := δpos n
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ R i ≤ M
have refine : R i ≤ (Finset.image R (Finset.range (n + 1))).max' sorry
Tactic: refine le_trans ?_ (le_max_left _ _)
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ R i ≤ (Finset.image R (Finset.range (n + 1))).max' ⋯
have H2 : R i ∈ Finset.image R (Finset.range (n + 1))
Tactic: apply Finset.le_max'
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ R i ∈ Finset.image R (Finset.range (n + 1))
have H2 : i ∈ Finset.range (n + 1)
Tactic: apply Finset.mem_image_of_mem
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
i : ℕ
hi : i ≤ n
⊢ i ∈ Finset.range (n + 1)
have H2 : i < n + 1
Tactic: simp only [Finset.mem_range]
-- 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_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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
⊢ ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
have IR : ∀ i ≤ n, R i ≤ M
Tactic: have IR : ∀ i ≤ n, R i ≤ M := by
      intro i hi
      refine le_trans ?_ (le_max_left _ _)
      apply Finset.le_max'
      apply Finset.mem_image_of_mem
      simp only [Finset.mem_range]
      lia
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
⊢ ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
have refine : ∀ (i : ℕ) (hi : i ≤ n) (x : E),
  norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) ≤
    (↑(δ n) : ℝ)
Tactic: refine ⟨M⁻¹ * δ n, by positivity, fun i hi 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
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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) =
    ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖
have rw : ContDiffAt ℝ (↑i : ℕ∞ω) (g n) x
Tactic: rw [iteratedFDeriv_const_smul_apply]
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
⊢ ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖ =
    M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x)
have rw : 0 ≤ M⁻¹ * (↑(δ n) : ℝ)
Tactic: rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
⊢ M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x) ≤
    M⁻¹ * (↑(δ n) : ℝ) * M
have hbc : norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x) ≤ M
Tactic: gcongr
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) ≤
    (↑(δ n) : ℝ)
have ℝ : norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) =
  ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
      (iteratedFDeriv ℝ i (g n) x)‖
Tactic: calc
      ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by
        rw [iteratedFDeriv_const_smul_apply]
        exact (g_smooth n).contDiffAt.of_le (mod_cast le_top)
      _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
        rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]; positivity
      _ ≤ M⁻¹ * δ n * M := by gcongr; exact (hR i x).trans (IR i hi)
      _ = δ n := by simp [field]
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
ℝ :
  norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) =
    ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) ≤
    (↑(δ n) : ℝ)
have ℝ₁ : ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
      (iteratedFDeriv ℝ i (g n) x)‖ =
  M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x)
Tactic: calc
      ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by
        rw [iteratedFDeriv_const_smul_apply]
        exact (g_smooth n).contDiffAt.of_le (mod_cast le_top)
      _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
        rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]; positivity
      _ ≤ M⁻¹ * δ n * M := by gcongr; exact (hR i x).trans (IR i hi)
      _ = δ n := by simp [field]
-- 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
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
ℝ :
  norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) =
    ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖
ℝ₁ :
  ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖ =
    M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x)
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) ≤
    (↑(δ n) : ℝ)
have ℝ₂ : M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x) ≤
  M⁻¹ * (↑(δ n) : ℝ) * M
Tactic: calc
      ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by
        rw [iteratedFDeriv_const_smul_apply]
        exact (g_smooth n).contDiffAt.of_le (mod_cast le_top)
      _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
        rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]; positivity
      _ ≤ M⁻¹ * δ n * M := by gcongr; exact (hR i x).trans (IR i hi)
      _ = δ n := by simp [field]