-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem _root_.Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {f : E → F}
    (hf_temperate : f.HasTemperateGrowth) (n : ℕ) :
    ∃ (k : ℕ) (C : ℝ), 0 ≤ C ∧ ∀ N ≤ n, ∀ x : E, ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Proof state:
case h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
⊢ ∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Tactic:
have hC' : 0 ≤ C' := by simp only [C', le_refl, Finset.le_sup'_iff, true_or, le_max_iff]

Result:
case h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
⊢ ∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Proof state:
case right
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
⊢ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C' * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Tactic:
intro N hN x

Result:
case right
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ≤ n
x : E
⊢ ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C' * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
hf_temperate : Function.HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k

Tactic:
choose k C f using hf_temperate.2

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
⊢ ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ k

Proof state:
case right.refine_2.ha
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ 1 ≤ 1 + ‖x‖

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ k N

Tactic:
positivity

Result:
no goals

Proof state:
case right.refine_1
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ C N ≤ 0 ∨ ∃ b ∈ Finset.range (n + 1), C N ≤ C b

Tactic:
right

Result:
case right.refine_1.h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ ∃ b ∈ Finset.range (n + 1), C N ≤ C b

Proof state:
case right
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C' * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Tactic:
refine le_trans (f N x) (mul_le_mul ?_ ?_ (by positivity) hC')

Result:
case right.refine_1
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ C N ≤ C'

case right.refine_2
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
hC' : 0 ≤ C'
N : ℕ
hN : N ∈ Finset.range n.succ
x : E
⊢ (1 + ‖x‖) ^ k N ≤ (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Proof state:
case h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
⊢ ∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Tactic:
let C' := max (0 : ℝ) ((Finset.range (n + 1)).sup' (by simp) C)

Result:
case h
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
⊢ ∃ C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f✝ x‖ ≤ C * (1 + ‖x‖) ^ (Finset.range (n + 1)).sup k

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f✝ : E → F
hf_temperate : Function.HasTemperateGrowth f✝
n : ℕ
k : ℕ → ℕ
C : ℕ → ℝ
f : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f✝ x‖ ≤ C n * (1 + ‖x‖) ^ k n
C' : ℝ := 0 ⊔ (Finset.range (n + 1)).sup' ⋯ C
⊢ 0 ≤ C'

Tactic:
simp only [C', le_refl, Finset.le_sup'_iff, true_or, le_max_iff]

Result:
no goals