-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem radius_le_radius_derivSeries : p.radius ≤ p.derivSeries.radius

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius ≤ p.derivSeries.radius

Tactic:
apply (p.le_changeOriginSeries_radius 1).trans (radius_le_of_le (fun n ↦ ?_))

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖p.derivSeries n‖ ≤ ‖p.changeOriginSeries 1 n‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ∀ (x : ContinuousMultilinearMap 𝕜 (fun i => E) F),
    ‖↑{ toLinearEquiv := (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }
          x‖ ≤
      1 * ‖x‖

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖↑{ toLinearEquiv := (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }‖ *
      ‖p.changeOriginSeries 1 n‖ ≤
    ‖p.changeOriginSeries 1 n‖

Tactic:
apply mul_le_of_le_one_left (norm_nonneg  _)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖↑{ toLinearEquiv := (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv, continuous_toFun := ⋯,
          continuous_invFun := ⋯ }‖ ≤
    1

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖p.derivSeries n‖ ≤ ‖p.changeOriginSeries 1 n‖

Tactic:
apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖↑{ toLinearEquiv := (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv, continuous_toFun := ⋯,
            continuous_invFun := ⋯ }‖ *
      ‖p.changeOriginSeries 1 n‖ ≤
    ‖p.changeOriginSeries 1 n‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖↑{ toLinearEquiv := (continuousMultilinearCurryFin1 𝕜 E F).toLinearEquiv, continuous_toFun := ⋯,
          continuous_invFun := ⋯ }‖ ≤
    1

Tactic:
exact ContinuousLinearMap.opNorm_le_bound _ zero_le_one (by simp)

Result:
no goals