-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : StarRing 𝕜
inst_8 : StarModule 𝕜 E
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
h₁ :
  ∀ (x : Unitization 𝕜 E),
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
h₂ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2 =
    HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 2
h₃ :
  norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).1 =
    HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2
h :
  norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2
pos :
  max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) *
      max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) ≤
    max
      (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1 *
        norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
      (HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2)
        2)
pos₁ :
  max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) *
      max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) ≤
    max
      (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1 *
        norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
      (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
        norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2)
pos₂ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    max
      (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1 *
        norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
      (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
        norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2)
pos₃ pos₄ :
  norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2 *
      norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2
⊢ max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) *
      max (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1)
        (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) ≤
    max (HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).1) 2)
      (HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2)
        2)

Tactic:
rw [sq, sq, sup_eq_right.mpr h, sup_eq_right.mpr (mul_self_le_mul_self (norm_nonneg _) h)]

Premises used: Iff.mpr, mul_self_le_mul_self, sq, sup_eq_right, norm_nonneg