-- Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
theorem norm_comp_le (g : W₂ →ᴬ[𝕜] V) : ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ 0 ≤ ‖f 0‖

Tactic:
apply norm_nonneg

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f (g 0)‖ = ‖f.contLinear (g 0) + f 0‖

Tactic:
rw [f.decomp]

Result:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(⇑f.contLinear + Function.const V (f 0)) (g 0)‖ = ‖f.contLinear (g 0) + (⇑f.contLinear + Function.const V (f 0)) 0‖

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
rw [le_add_iff_nonneg_right]

Result:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ 0 ≤ ‖f 0‖

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ ∧ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
constructor

Result:
case left
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

case right
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Proof state:
case left
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
calc
  ‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
  _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
  _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ :=
    ((norm_add_le _ _).trans (add_le_add_right (f.contLinear.le_opNorm _) _))
  _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ :=
    add_le_add_right
      (mul_le_mul f.norm_contLinear_le g.norm_image_zero_le (norm_nonneg _) (norm_nonneg _)) _

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ = ‖f (g 0)‖

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(⇑f.contLinear + Function.const V (f 0)) (g 0)‖ = ‖f.contLinear (g 0) + (⇑f.contLinear + Function.const V (f 0)) 0‖

Tactic:
simp

Result:
no goals

Proof state:
case right
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
calc
  ‖(f.comp g).contLinear‖ ≤ ‖f.contLinear‖ * ‖g.contLinear‖ :=
    (g.comp_contLinear f).symm ▸ f.contLinear.opNorm_comp_le _
  _ ≤ ‖f‖ * ‖g‖ :=
    (mul_le_mul f.norm_contLinear_le g.norm_contLinear_le (norm_nonneg _) (norm_nonneg _))
  _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by rw [le_add_iff_nonneg_right]; apply norm_nonneg

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
rw [norm_def, max_le_iff]

Result:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ ∧ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖