awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ a * ⟪x, x⟫_A * star a ≤ ‖⟪x, x⟫_A‖ •> (a * star a)

Tactic:
CStarAlgebra.star_right_conjugate_le_norm_smul

Premises used: CStarAlgebra.star_right_conjugate_le_norm_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
rw : 0 ≤ ‖⟪x, x⟫_A‖
⊢ ‖⟪x, x⟫_A‖ •> (a * star a) = HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a)

Tactic:
rw [Real.sq_sqrt]

Premises used: Real.sq_sqrt
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
⊢ 0 ≤ ‖⟪x, x⟫_A‖

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
rw rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) = HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
⊢ HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a) = HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)

Tactic:
rw [← norm_eq_sqrt_norm_inner_self]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
calc : ‖⟪x, x⟫_A‖ •> (a * star a) = HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a)
calc₁ : HPow.hPow (β := ℕ) (√‖⟪x, x⟫_A‖) 2 •> (a * star a) = HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)
⊢ a * ⟪x, x⟫_A * star a ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a)

Tactic:
calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]

Premises used: Norm.norm, HMul.hMul, Inner.inner, Real.sqrt, CStarAlgebra.star_right_conjugate_le_norm_smul, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
a : A
calc : 0 ≤ ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A
calc₁ :
  ⟪a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y, a •> x - HPow.hPow (β := ℕ) ‖x‖ 2 •> y⟫_A =
    a * ⟪x, x⟫_A * star a - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
calc₂ :
  a * ⟪x, x⟫_A * star a - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ 0 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖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, mul_sub, mul_smul_comm,
                        inner_smul_right_real, smul_sub, mul_assoc]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]

Premises used: HMul.hMul, OfNat.ofNat, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
⊢ ∀ (a : A),
    0 ≤
      HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
          HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
        HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
have h₁ : ∀ (a : A),
        (0 : A) ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := fun a => by
      calc (0 : A) ≤ ⟪a • x - ‖x‖ ^ 2 • y, a • x - ‖x‖ ^ 2 • y⟫_A := by
                      exact inner_self_nonneg
            _ = a * ⟪x, x⟫ * star a - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖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, mul_sub, mul_smul_comm,
                        inner_smul_right_real, smul_sub, mul_assoc]
                      abel
            _ ≤ ‖x‖ ^ 2 • (a * star a) - ‖x‖ ^ 2 • (a * ⟪y, x⟫)
                  - ‖x‖ ^ 2 • (⟪x, y⟫ * star a) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                      gcongr
                      calc _ ≤ ‖⟪x, x⟫_A‖ • (a * star a) :=
                          CStarAlgebra.star_right_conjugate_le_norm_smul
                        _ = (√‖⟪x, x⟫_A‖) ^ 2 • (a * star a) := by
                          rw [Real.sq_sqrt]
                          positivity
                        _ = ‖x‖ ^ 2 • (a * star a) := by rw [← norm_eq_sqrt_norm_inner_self]
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
h₁ :
  ∀ (a : A),
    0 ≤
      HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * star a) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (a * ⟪y, x⟫_A) -
          HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star a) +
        HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ 0 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

Tactic:
specialize h₁ ⟪x, y⟫
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
h₁ :
  0 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) - HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) -
        HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * star ⟪x, y⟫_A) +
      HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

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

Premises used: sub_self, CStarModule.star_inner, add_zero, le_neg_add_iff_add_le, zero_sub
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
h : x ≠ 0
h₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 •> (⟪x, y⟫_A * ⟪y, x⟫_A) ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
inr inr₁ inr₂ inr₃ :
  ∀ (h₁ : ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A),
    ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A
⊢ ⟪x, y⟫_A * ⟪y, x⟫_A ≤ HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A

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

Premises used: pow_pos, smul_le_smul_iff_of_pos_left, CStarModule.norm_pos
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
rw : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * star ⟪x, y⟫_A‖
rw₁ : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖
rw₂ rw₃ : ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖ = ‖⟪x, y⟫_A‖ * ‖⟪x, y⟫_A‖
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 = ‖⟪x, y⟫_A * ⟪y, x⟫_A‖

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

Premises used: pow_two, CStarModule.star_inner, CStarRing.norm_self_mul_star
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, y⟫_A * ⟪y, x⟫_A‖ ≤ ‖HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A‖

Tactic:
CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le, CStarModule.inner_mul_inner_swap_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
refine : 0 ≤ ⟪x, y⟫_A * ⟪y, x⟫_A
⊢ ‖⟪x, y⟫_A * ⟪y, x⟫_A‖ ≤ ‖HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A‖

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le

Premises used: CStarAlgebra.norm_le_norm_of_nonneg_of_le, CStarModule.inner_mul_inner_swap_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
rw : 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A
⊢ 0 ≤ ⟪x, y⟫_A * ⟪y, x⟫_A

Tactic:
rw [← star_inner x]

Premises used: CStarModule.star_inner
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A

Tactic:
mul_star_self_nonneg ⟪x, y⟫_A

Premises used: Inner.inner, mul_star_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A

Tactic:
exact mul_star_self_nonneg ⟪x, y⟫_A

Premises used: Inner.inner, mul_star_self_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖HPow.hPow (β := ℕ) ‖x‖ 2 •> ⟪y, y⟫_A‖ = HPow.hPow (β := ℕ) ‖x‖ 2 * ‖⟪y, y⟫_A‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * ‖⟪y, y⟫_A‖ = HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
simp only [norm_eq_sqrt_norm_inner_self (A := A), norm_nonneg, Real.sq_sqrt]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self, Real.sq_sqrt, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2

Tactic:
simp only [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2

Tactic:
have := calc ‖⟪x, y⟫‖ ^ 2 = ‖⟪x, y⟫ * ⟪y, x⟫‖ := by
                rw [← star_inner x, CStarRing.norm_self_mul_star, 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 mul_star_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 (A := A), norm_nonneg, Real.sq_sqrt]
    _ = (‖x‖ * ‖y‖) ^ 2 := by simp only [mul_pow]
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
this : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
this : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
refine : 0 ≤ ‖x‖ * ‖y‖
⊢ ‖⟪x, y⟫_A‖ ≤ ‖x‖ * ‖y‖

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

Premises used: Inner.inner, pow_le_pow_iff_left₀, Iff.mp, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
this : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
mul_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)

Premises used: mul_nonneg, CStarModule.norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
this : HPow.hPow (β := ℕ) ‖⟪x, y⟫_A‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
exact mul_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)

Premises used: mul_nonneg, CStarModule.norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
simp : ‖⟪x, x⟫ + ⟪y, x⟫ + ⟪x, y⟫ + ⟪y, y⟫‖ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖

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

Premises used: add_assoc, CStarModule.norm_eq_sqrt_norm_inner_self, Real.sq_sqrt, CStarModule.inner_add_left, CStarModule.inner_add_right, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, x⟫ + ⟪y, x⟫ + ⟪x, y⟫ + ⟪y, y⟫‖ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖

Tactic:
norm_add₃_le

Premises used: norm_add₃_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, x⟫ + ⟪y, x⟫ + ⟪x, y⟫ + ⟪y, y⟫‖ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖

Tactic:
exact norm_add₃_le

Premises used: norm_add₃_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
bc : ‖⟪x, x⟫ + ⟪y, x⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖
⊢ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, x⟫ + ⟪y, x⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, x⟫ + ⟪y, x⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖

Tactic:
exact norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
bc : ‖⟪y, x⟫‖ ≤ ‖y‖ * ‖x‖
bc₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
⊢ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪y, x⟫‖ ≤ ‖y‖ * ‖x‖

Tactic:
norm_inner_le E

Premises used: CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪y, x⟫‖ ≤ ‖y‖ * ‖x‖

Tactic:
exact norm_inner_le E

Premises used: CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
norm_inner_le E

Premises used: CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
exact norm_inner_le E

Premises used: CStarModule.norm_inner_le
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ =
    HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
simp [norm_eq_sqrt_norm_inner_self (A := A)]

Premises used: CStarModule.norm_eq_sqrt_norm_inner_self
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
simp : HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ = HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2

Tactic:
simp only [add_pow_two, add_left_inj]

Premises used: add_left_inj, add_pow_two
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ = HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖

Tactic:
ring
-- Module: Mathlib.Analysis.CStarAlgebra.Module.Defs
Goal:
A : Type u_1
E : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : AddCommGroup E
inst_3 : Module ℂ E
inst_4 : SMul A E
inst_5 : Norm E
inst_6 : CStarModule A E
inst_7 : StarOrderedRing A
x y : E
calc : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₁ : ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖
calc₂ : ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖
calc₃ :
  ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ =
    HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2
calc₄ : HPow.hPow (β := ℕ) ‖x‖ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2

Tactic:
calc _ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by
          simp only [norm_eq_sqrt_norm_inner_self (A := A), 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 (A := A)]
      _ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring

Premises used: Norm.norm, HAdd.hAdd