Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply (ForML/SchwartzEquiv.lean)

State before:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
suffices : ‖e.symm.toContinuousLinearMap (e x)‖ ≤ ‖e.symm.toContinuousLinearMap‖ * ‖e x‖
State after:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
this : ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

State before:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
this : ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
. simpa
State after:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

State before:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
refine le_trans (ContinuousLinearMap.le_opNorm _ _) ?_
State after:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

State before:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
refine mul_le_mul_of_nonneg_left ?_ (norm_nonneg _)
State after:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖e x‖ ≤ ‖e x‖

State before:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖e x‖ ≤ ‖e x‖
Tactic:
simp [le_add_iff_nonneg_left]
State after:
no goals

State before:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
this : ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
simpa
State after:
no goals