-- Mathlib/Analysis/CStarAlgebra/Unitization.lean
theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
    ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤ ‖(Unitization.splitMul 𝕜 E (star x * x)).snd‖

Proof state:
case intro.intro.calc_1
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ BddAbove
    ((fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) x_1‖) '' Metric.closedBall 0 1)

Tactic:
refine ⟨‖(star x * x).fst‖ + ‖(star x * x).snd‖, ?_⟩

Result:
case intro.intro.calc_1
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖(x⋆ * x).fst‖ + ‖(x⋆ * x).snd‖ ∈
    upperBounds
      ((fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) x_1‖) '' Metric.closedBall 0 1)

Proof state:
case intro.intro.calc_1.intro.intro.h₁
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖↑((x⋆ * x).fst • 1) y‖ ≤ ‖(x⋆ * x).fst‖

Tactic:
refine (norm_smul _ _).trans_le ?_

Result:
case intro.intro.calc_1.intro.intro.h₁
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖(x⋆ * x).fst‖ * ‖↑1 y‖ ≤ ‖(x⋆ * x).fst‖

Proof state:
case intro.intro.calc_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖(x.fst⋆ * x.fst) • b + (x.fst⋆ • x.snd * b + x.fst • x.snd⋆ * b + x.snd⋆ * x.snd * b)‖ =
    ‖x.fst⋆ • x.fst • b + x.fst⋆ • (x.snd * b) + (x.snd⋆ * x.fst • b + x.snd⋆ * (x.snd * b))‖

Tactic:
simp only [smul_smul, smul_mul_assoc, ← add_assoc, ← mul_assoc, mul_smul_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ∀ b ∈ (fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) x_1‖) '' Metric.closedBall 0 1,
    b ≤ √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖

Tactic:
rintro - ⟨b, hb, rfl⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ (fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) x_1‖) b ≤
    √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖b⋆‖ ≤ 1

Tactic:
exact (norm_star b).symm ▸ mem_closedBall_zero_iff.1 hb

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ (fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) x_1‖) b ≤
    √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖

Tactic:
simp only

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
⊢ ‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) b‖ ≤
    √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖

Proof state:
case intro.intro.calc_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ (fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) x_1‖) y ≤
    ‖(x⋆ * x).fst‖ + ‖(x⋆ * x).snd‖

Tactic:
refine (norm_add_le _ _).trans ?_

Result:
case intro.intro.calc_1.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
b : E
hb : b ∈ Metric.closedBall 0 1
y : E
hy : y ∈ Metric.closedBall 0 1
⊢ ‖↑((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst) y‖ + ‖↑((mul 𝕜 E) (x⋆ * x).snd) y‖ ≤ ‖(x⋆ * x).fst‖ + ‖(x⋆ * x).snd‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ‖((splitMul 𝕜 E) x).2‖ ≤ √‖((splitMul 𝕜 E) (x⋆ * x)).2‖

Tactic:
simp only [Unitization.splitMul_apply]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd‖ ≤
    √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ‖((splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖

Tactic:
refine (Real.le_sqrt (norm_nonneg _) (norm_nonneg _)).mp ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : NonUnitalNormedRing E
inst✝⁶ : StarRing E
inst✝⁵ : CStarRing E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : IsScalarTower 𝕜 E E
inst✝² : SMulCommClass 𝕜 E E
inst✝¹ : StarRing 𝕜
inst✝ : StarModule 𝕜 E
x : Unitization 𝕜 E
⊢ ‖((splitMul 𝕜 E) x).2‖ ≤ √‖((splitMul 𝕜 E) (x⋆ * x)).2‖