-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
/-- The C⋆-algebra-valued Cauchy-Schwarz inequality for Hilbert C⋆-modules. -/
lemma inner_mul_inner_swap_le {x y : E} : ⟪y, x⟫ * ⟪x, y⟫ ≤ ‖x‖ ^ 2 • ⟪y, y⟫

Proof state:
case inr
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 ≠ 0
h₁ :
  ∀ (a : A),
    0 ≤
      ‖x‖ ^ 2 •> (star a * a) - ‖x‖ ^ 2 •> (⟪y, x⟫_A * a) - ‖x‖ ^ 2 •> (star a * ⟪x, y⟫_A) +
        ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A
⊢ ⟪y, x⟫_A * ⟪x, y⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
specialize h₁ ⟪x, y⟫

Result:
case inr
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 ≠ 0
h₁ :
  0 ≤
    ‖x‖ ^ 2 •> (star ⟪x, y⟫_A * ⟪x, y⟫_A) - ‖x‖ ^ 2 •> (⟪y, x⟫_A * ⟪x, y⟫_A) - ‖x‖ ^ 2 •> (star ⟪x, y⟫_A * ⟪x, y⟫_A) +
      ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A
⊢ ⟪y, x⟫_A * ⟪x, y⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A

Proof state:
case e_a
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 ≠ 0
a : A
this : 0 ≤ ‖⟪x, x⟫_A‖
⊢ ‖⟪x, x⟫_A‖ = √‖⟪x, x⟫_A‖ ^ 2

Tactic:
rw [Real.sq_sqrt this]

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 ≠ 0
a : A
⊢ 0 ≤ ‖⟪x, x⟫_A‖

Tactic:
positivity

Result:
no goals

Proof state:
case e_a
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 ≠ 0
a : A
⊢ ‖⟪x, x⟫_A‖ = √‖⟪x, x⟫_A‖ ^ 2

Tactic:
have : 0 ≤ ‖⟪x, x⟫_A‖ := by positivity

Result:
case e_a
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 ≠ 0
a : A
this : 0 ≤ ‖⟪x, x⟫_A‖
⊢ ‖⟪x, x⟫_A‖ = √‖⟪x, x⟫_A‖ ^ 2

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 ≠ 0
a : A
⊢ 0 ≤ ⟪x <• a - ‖x‖ ^ 2 •> y, x <• a - ‖x‖ ^ 2 •> y⟫_A

Tactic:
exact inner_self_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
h : x ≠ 0
a : A
⊢ √‖⟪x, x⟫_A‖ ^ 2 •> (star a * a) = ‖x‖ ^ 2 •> (star a * a)

Tactic:
rw [← 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
h : x ≠ 0
a : A
⊢ star a * ⟪x, x⟫_A * a - ‖x‖ ^ 2 •> (⟪y, x⟫_A * a) -
      (‖x‖ ^ 2 •> (star a * ⟪x, y⟫_A) - ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A) =
    star a * ⟪x, x⟫_A * a - ‖x‖ ^ 2 •> (⟪y, x⟫_A * a) - ‖x‖ ^ 2 •> (star a * ⟪x, y⟫_A) + ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
abel

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 ≠ 0
a : A
⊢ 0 ≤
    ‖x‖ ^ 2 •> (star a * a) - ‖x‖ ^ 2 •> (⟪y, x⟫_A * a) - ‖x‖ ^ 2 •> (star a * ⟪x, y⟫_A) +
      ‖x‖ ^ 2 •> ‖x‖ ^ 2 •> ⟪y, y⟫_A

Tactic:
calc (0 : A) ≤ ⟪x <• a - ‖x‖ ^ 2 • y, x <• a - ‖x‖ ^ 2 • y⟫_A := by
                exact inner_self_nonneg
      _ = star a * ⟪x, x⟫ * a - ‖x‖ ^ 2 • (⟪y, x⟫ * a)
            - ‖x‖ ^ 2 • (star a * ⟪x, y⟫) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                simp only [inner_sub_right, inner_op_smul_right, inner_sub_left,
                  inner_op_smul_left, inner_smul_left_real, sub_mul, smul_mul_assoc,
                  inner_smul_right_real, smul_sub]
                abel
      _ ≤ ‖x‖ ^ 2 • (star a * a) - ‖x‖ ^ 2 • (⟪y, x⟫ * a)
            - ‖x‖ ^ 2 • (star a * ⟪x, y⟫) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                gcongr
                calc _ ≤ ‖⟪x, x⟫_A‖ • (star a * a) := CStarAlgebra.conjugate_le_norm_smul
                  _ = (Real.sqrt ‖⟪x, x⟫_A‖) ^ 2 • (star a * a) := by
                            congr
                            have : 0 ≤ ‖⟪x, x⟫_A‖ := by positivity
                            rw [Real.sq_sqrt this]
                  _ = ‖x‖ ^ 2 • (star a * a) := by rw [← 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
h : x ≠ 0
a : A
⊢ ‖⟪x, x⟫_A‖ •> (star a * a) = √‖⟪x, x⟫_A‖ ^ 2 •> (star a * a)

Tactic:
congr

Result:
case e_a
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 ≠ 0
a : A
⊢ ‖⟪x, x⟫_A‖ = √‖⟪x, x⟫_A‖ ^ 2

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:
rcases eq_or_ne x 0 with h|h

Result:
case inl
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 = 0
⊢ ⟪y, x⟫_A * ⟪x, y⟫_A ≤ ‖x‖ ^ 2 •> ⟪y, y⟫_A

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