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

Tactic:
have h₁ : ∀ (a : A),
    (0 : A) ≤ ‖x‖ ^ 2 • (star a * a) - ‖x‖ ^ 2 • (⟪y, x⟫ * a)
              - ‖x‖ ^ 2 • (star a * ⟪x, y⟫) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := fun a => by
  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:
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

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 ≤
    ‖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:
gcongr

Result:
case bc.h.h
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 •> (star a * a)

Proof state:
case bc.h.h
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 •> (star a * a)

Tactic:
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:
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

Tactic:
simp only [star_inner, sub_self, zero_sub, le_neg_add_iff_add_le, add_zero] at h₁

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

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 ≠ 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

Proof state:
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

Tactic:
simp [h, CStarModule.norm_zero (E := E)]

Result:
no goals

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

Tactic:
rwa [smul_le_smul_iff_of_pos_left (pow_pos (CStarModule.norm_pos h) _)] at h₁

Result:
no goals