-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
/-- The Cauchy-Schwarz inequality for Hilbert C⋆-modules. -/
lemma norm_inner_le {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
this : ‖⟪x, y⟫_A‖ ^ 2 ≤ (‖x‖ * ‖y‖) ^ 2
⊢ ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖

Tactic:
refine (pow_le_pow_iff_left₀ (norm_nonneg ⟪x, y⟫_A) ?_ (by norm_num)).mp this

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
this : ‖⟪x, y⟫_A‖ ^ 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
⊢ 0 ≤ ⟪y, x⟫_A * ⟪x, y⟫_A

Tactic:
rw [← star_inner x]

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
⊢ 0 ≤ star ⟪x, y⟫_A * ⟪x, y⟫_A

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
this : ‖⟪x, y⟫_A‖ ^ 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
⊢ ‖‖x‖ ^ 2 •> ⟪y, y⟫_A‖ = ‖x‖ ^ 2 * ‖⟪y, y⟫_A‖

Tactic:
simp [norm_smul]

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
⊢ ‖⟪y, x⟫_A * ⟪x, y⟫_A‖ ≤ ‖‖x‖ ^ 2 •> ⟪y, y⟫_A‖

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le

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
⊢ 0 ≤ ⟪y, x⟫_A * ⟪x, y⟫_A

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, y⟫_A‖ = ‖x‖ ^ 2 * ‖y‖ ^ 2

Tactic:
simp only [norm_eq_sqrt_norm_inner_self, norm_nonneg, Real.sq_sqrt]

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
⊢ 0 ≤ star ⟪x, y⟫_A * ⟪x, y⟫_A

Tactic:
exact star_mul_self_nonneg ⟪x, y⟫_A

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⟫_A‖ ^ 2 = ‖⟪y, x⟫_A * ⟪x, y⟫_A‖

Tactic:
rw [← star_inner x, CStarRing.norm_star_mul_self, pow_two]

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
this : ‖⟪x, y⟫_A‖ ^ 2 ≤ (‖x‖ * ‖y‖) ^ 2
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
exact mul_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‖ ^ 2 = (‖x‖ * ‖y‖) ^ 2

Tactic:
simp only [mul_pow]

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⟫_A‖ ≤ ‖x‖ * ‖y‖

Tactic:
have := calc ‖⟪x, y⟫‖ ^ 2 = ‖⟪y, x⟫ * ⟪x, y⟫‖ := by
              rw [← star_inner x, CStarRing.norm_star_mul_self, pow_two]
  _ ≤ ‖‖x‖^ 2 • ⟪y, y⟫‖ := by
              refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
              rw [← star_inner x]
              exact star_mul_self_nonneg ⟪x, y⟫_A
  _ = ‖x‖ ^ 2 * ‖⟪y, y⟫‖ := by simp [norm_smul]
  _ = ‖x‖ ^ 2 * ‖y‖ ^ 2 := by
              simp only [norm_eq_sqrt_norm_inner_self, norm_nonneg, Real.sq_sqrt]
  _ = (‖x‖ * ‖y‖) ^ 2 := by simp only [mul_pow]

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
this : ‖⟪x, y⟫_A‖ ^ 2 ≤ (‖x‖ * ‖y‖) ^ 2
⊢ ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖