awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i : ℕ
hi : i ≤ n
⊢ C₂ * (1 + ‖f x‖) ^ k₂ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ))
have rw : Eq (α := ℝ) (∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * HPow.hPow (α := ℝ) 1 (k₂ - i) * (↑(k₂.choose i) : ℝ)))
  (∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ)))
Tactic: rw [add_comm, add_pow, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i : ℕ
hi : i ≤ n
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ)))
    (∑ i ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂))
have h : ∀ i ∈ Finset.range (k₂ + 1),
  C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ)) ≤ C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
Tactic: apply Finset.sum_le_sum
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i_1 : ℕ
hi_1 : i_1 ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
⊢ C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ)) ≤ C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
have h : C₂ * ((C₁ * (1 + ‖x‖) ^ k₁) ^ i * (↑(k₂.choose i) : ℝ)) ≤ C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
Tactic: grw [h₁']
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i_1 : ℕ
hi_1 : i_1 ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
⊢ C₂ * ((C₁ * (1 + ‖x‖) ^ k₁) ^ i * (↑(k₂.choose i) : ℝ)) ≤ C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
have h : C₂ * (C₁ ^ i * (1 + ‖x‖) ^ (k₁ * i) * (↑(k₂.choose i) : ℝ)) ≤ C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
Tactic: simp_rw [mul_pow, ← pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i_1 : ℕ
hi_1 : i_1 ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
⊢ C₂ * (C₁ ^ i * (1 + ‖x‖) ^ (k₁ * i) * (↑(k₂.choose i) : ℝ)) ≤
    C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂)
have h : (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * i) * C₂ ≤ (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) * C₂
Tactic: move_mul [← (k₂.choose _ : ℝ), C₂]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i_1 : ℕ
hi_1 : i_1 ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
⊢ (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * i) * C₂ ≤ (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) * C₂
have h : 1 ≤ 1 + ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i_1 : ℕ
hi_1 : i_1 ≤ n
i : ℕ
hi : i ∈ Finset.range (k₂ + 1)
h : 1 ≤ 1 + ‖x‖
⊢ (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * i) * C₂ ≤ (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) * C₂
have h₃ : i ≤ k₂
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i : ℕ
hi : i ≤ n
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin ℝ i g t (f x)) ≤
    C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
have calc : C₂ * (1 + ‖f x‖) ^ k₂ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ))
Tactic: calc _ ≤ C₂ * (1 + ‖f x‖) ^ k₂ := h₂ i hi (f x) (ht ⟨x, rfl⟩)
      _ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (k₂.choose i)) := by
        rw [add_comm, add_pow, Finset.mul_sum]
        simp
      _ ≤ ∑ i ∈ Finset.range (k₂ + 1), C₂ * (k₂.choose i) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) := by
        apply Finset.sum_le_sum
        intro i hi
        grw [h₁']
        simp_rw [mul_pow, ← pow_mul]
        move_mul [← (k₂.choose _ : ℝ), C₂]
        gcongr
        · simp
        · grind
      _ = _ := by simp [C₃, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i : ℕ
hi : i ≤ n
calc : C₂ * (1 + ‖f x‖) ^ k₂ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ))
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin ℝ i g t (f x)) ≤
    C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
have calc₁ : LE.le (α := ℝ) (∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ)))
  (∑ i ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂))
Tactic: calc _ ≤ C₂ * (1 + ‖f x‖) ^ k₂ := h₂ i hi (f x) (ht ⟨x, rfl⟩)
      _ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (k₂.choose i)) := by
        rw [add_comm, add_pow, Finset.mul_sum]
        simp
      _ ≤ ∑ i ∈ Finset.range (k₂ + 1), C₂ * (k₂.choose i) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) := by
        apply Finset.sum_le_sum
        intro i hi
        grw [h₁']
        simp_rw [mul_pow, ← pow_mul]
        move_mul [← (k₂.choose _ : ℝ), C₂]
        gcongr
        · simp
        · grind
      _ = _ := by simp [C₃, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
i : ℕ
hi : i ≤ n
calc : C₂ * (1 + ‖f x‖) ^ k₂ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ))
calc₁ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (↑(k₂.choose i) : ℝ)))
    (∑ i ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂))
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin ℝ i g t (f x)) ≤
    C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
have calc₂ : ∑ i ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose i) : ℝ) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) = C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
Tactic: calc _ ≤ C₂ * (1 + ‖f x‖) ^ k₂ := h₂ i hi (f x) (ht ⟨x, rfl⟩)
      _ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (k₂.choose i)) := by
        rw [add_comm, add_pow, Finset.mul_sum]
        simp
      _ ≤ ∑ i ∈ Finset.range (k₂ + 1), C₂ * (k₂.choose i) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) := by
        apply Finset.sum_le_sum
        intro i hi
        grw [h₁']
        simp_rw [mul_pow, ← pow_mul]
        move_mul [← (k₂.choose _ : ℝ), C₂]
        gcongr
        · simp
        · grind
      _ = _ := by simp [C₃, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (hypothesis)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F) (iteratedFDeriv ℝ n (g ∘ f) x) ≤
    (↑n ! : ℝ) * C₃ * (1 + C₁) ^ n * (1 + ‖x‖) ^ (k₁ * k₂ + k₁ * n)
have hg' : ∀ i ≤ n,
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F) (iteratedFDerivWithin ℝ i g t (f x)) ≤
    C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
Tactic: have hg' : ∀ i, i ≤ n → ‖iteratedFDerivWithin ℝ i g t (f x)‖ ≤ C₃ * (1 + ‖x‖) ^ (k₁ * k₂) := by
    intro i hi
    calc _ ≤ C₂ * (1 + ‖f x‖) ^ k₂ := h₂ i hi (f x) (ht ⟨x, rfl⟩)
      _ = ∑ i ∈ Finset.range (k₂ + 1), C₂ * (‖f x‖ ^ i * (k₂.choose i)) := by
        rw [add_comm, add_pow, Finset.mul_sum]
        simp
      _ ≤ ∑ i ∈ Finset.range (k₂ + 1), C₂ * (k₂.choose i) * C₁ ^ i * (1 + ‖x‖) ^ (k₁ * k₂) := by
        apply Finset.sum_le_sum
        intro i hi
        grw [h₁']
        simp_rw [mul_pow, ← pow_mul]
        move_mul [← (k₂.choose _ : ℝ), C₂]
        gcongr
        · simp
        · grind
      _ = _ := by simp [C₃, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ C₁ * (1 + ‖x‖) ^ k₁ ≤ (1 + C₁) * (1 + ‖x‖) ^ k₁
have hbc : C₁ ≤ 1 + C₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.TemperateGrowth (goal)
Goal:
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup D
inst_5 : NormedSpace ℝ D
g : E → F
f : D → E
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ :
  ∀ (N : ℕ),
    ∃ (k : ℕ) (C : ℝ) (_ : 0 ≤ C),
      ∀ n ≤ N,
        ∀ x ∈ t,
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDerivWithin ℝ n g t x) ≤
            C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n k₁ : ℕ
C₁ : ℝ
hC₁ : 0 ≤ C₁
h₁ :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N f x) ≤
        C₁ * (1 + ‖x‖) ^ k₁
k₂ : ℕ
C₂ : ℝ
hC₂ : 0 ≤ C₂
h₂ :
  ∀ n_1 ≤ n,
    ∀ x ∈ t,
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n_1) ↦ E) F)
          (iteratedFDerivWithin ℝ n_1 g t x) ≤
        C₂ * (1 + ‖x‖) ^ k₂
h₁' : ∀ (x : D), ‖f x‖ ≤ C₁ * (1 + ‖x‖) ^ k₁
C₃ : ℝ := ∑ k ∈ Finset.range (k₂ + 1), C₂ * (↑(k₂.choose k) : ℝ) * C₁ ^ k
x : D
hg' :
  ∀ i ≤ n,
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDerivWithin ℝ i g t (f x)) ≤
      C₃ * (1 + ‖x‖) ^ (k₁ * k₂)
i : ℕ
hi : 1 ≤ i
hi' : i ≤ n
⊢ (1 + C₁) * (1 + ‖x‖) ^ k₁ ≤ ((1 + C₁) * (1 + ‖x‖) ^ k₁) ^ i
have apply : i ≠ 0
Tactic: apply le_self_pow₀ (one_le_mul_of_one_le_of_one_le (by simp [hC₁]) (by simp [one_le_pow₀]))