-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
protected lemma norm_triangle (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2
⊢ 0 ≤ ‖x‖ + ‖y‖

Tactic:
exact add_nonneg CStarModule.norm_nonneg CStarModule.norm_nonneg

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ = ‖x‖ ^ 2 + 2 * ‖x‖ * ‖y‖

Tactic:
ring

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x‖ + ‖inner y x‖ + ‖inner x y‖ + ‖inner y y‖ ≤ ‖inner x x‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖inner y y‖

Tactic:
gcongr <;> exact norm_inner_le E

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
refine (pow_le_pow_iff_left₀ CStarModule.norm_nonneg ?_ (by norm_num)).mp h

Result:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2
⊢ 0 ≤ ‖x‖ + ‖y‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x + inner y x + inner x y + inner y y‖ ≤ ‖inner x x + inner y x‖ + ‖inner x y‖ + ‖inner y y‖

Tactic:
exact norm_add₃_le

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖inner y y‖ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2

Tactic:
simp [norm_eq_sqrt_norm_inner_self]

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2

Tactic:
calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
      simp only [norm_eq_sqrt_norm_inner_self, inner_add_right, inner_add_left, ← add_assoc,
        norm_nonneg, Real.sq_sqrt]
      exact norm_add₃_le
  _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
  _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
  _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
      simp [norm_eq_sqrt_norm_inner_self]
  _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x + y‖ ^ 2 ≤ ‖inner x x + inner y x‖ + ‖inner x y‖ + ‖inner y y‖

Tactic:
simp only [norm_eq_sqrt_norm_inner_self, inner_add_right, inner_add_left, ← add_assoc,
  norm_nonneg, Real.sq_sqrt]

Result:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x + inner y x + inner x y + inner y y‖ ≤ ‖inner x x + inner y x‖ + ‖inner x y‖ + ‖inner y y‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x + inner y x‖ + ‖inner x y‖ + ‖inner y y‖ ≤ ‖inner x x‖ + ‖inner y x‖ + ‖inner x y‖ + ‖inner y y‖

Tactic:
gcongr

Result:
case bc.bc
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x + inner y x‖ ≤ ‖inner x x‖ + ‖inner y x‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
simp only [add_pow_two, add_left_inj]

Result:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ = ‖x‖ ^ 2 + 2 * ‖x‖ * ‖y‖

Proof state:
case bc.bc
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖inner x x + inner y x‖ ≤ ‖inner x x‖ + ‖inner y x‖

Tactic:
exact norm_add_le _ _

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖

Tactic:
have h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2 := by
  calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
        simp only [norm_eq_sqrt_norm_inner_self, inner_add_right, inner_add_left, ← add_assoc,
          norm_nonneg, Real.sq_sqrt]
        exact norm_add₃_le
    _ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
    _ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
    _ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by
        simp [norm_eq_sqrt_norm_inner_self]
    _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring

Result:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖