awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
rw :
  ‖b⋆ * (x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b))‖ ≤
    sSup
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)
⊢ norm (E := E)
      ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) x.toProd.1 : E →L[𝕜] E)
              ((mul 𝕜 E : (a : E) → E →L[𝕜] E) x.toProd.2 : E →L[𝕜] E) :
            (a : E) → E)
          b :
        E) ≤
    √‖HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
          ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
          ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E)‖

Tactic:
rw [← Real.sqrt_sq (norm_nonneg _), Real.sqrt_le_sqrt_iff (norm_nonneg _), sq,
    ← CStarRing.norm_star_mul_self, ContinuousLinearMap.add_apply, star_add, mul_apply',
    Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply,
    ContinuousLinearMap.one_apply, star_mul, star_smul, add_mul, smul_mul_assoc, ← mul_smul_comm,
    mul_assoc, ← mul_add, ← sSup_unitClosedBall_eq_norm]

Premises used: add_mul, ContinuousLinearMap.smul_apply, StarAddMonoid.star_add, StarModule.star_smul, mul_assoc, Real.sqrt_le_sqrt_iff, ContinuousLinearMap.add_apply, smul_mul_assoc, ContinuousLinearMap.one_apply, sq, Algebra.algebraMap_eq_smul_one, CStarRing.norm_star_mul_self, ContinuousLinearMap.mul_apply', StarMul.star_mul, Real.sqrt_sq, mul_smul_comm, mul_add, ContinuousLinearMap.sSup_unitClosedBall_eq_norm, norm_nonneg
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
⊢ ‖b⋆ * (x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b))‖ ≤
    sSup
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)

Tactic:
(norm_mul_le _ _).trans ?_

Premises used: LE.le.trans, norm_mul_le
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
refine :
  ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    sSup
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)
⊢ ‖b⋆ * (x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b))‖ ≤
    sSup
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)

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

Premises used: LE.le.trans, norm_mul_le
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
nth_rewrite :
  ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    1 * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖
⊢ ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖

Tactic:
nth_rewrite 2 [← one_mul ‖_ + _‖]

Premises used: Norm.norm, HAdd.hAdd, one_mul
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
hbc : ‖b⋆‖ ≤ 1
⊢ ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    1 * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖

Tactic:
gcongr
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
⊢ ‖b⋆‖ ≤ 1

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

Premises used: norm_star, Eq.rec, Iff.mp, mem_closedBall_zero_iff, Eq.symm
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
⊢ ‖b⋆‖ ≤ 1

Tactic:
exact (norm_star b).symm ▸ mem_closedBall_zero_iff.1 hb
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
⊢ ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    sSup
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)

Tactic:
le_csSup ?_ ⟨b, hb, ?_⟩

Premises used: And.intro, Exists.intro, le_csSup
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
calc_1 :
  BddAbove (α := ℝ)
    ((fun (x_1 : E) ↦
        norm (E := E)
          ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                  ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                  ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                (a : E) → E)
              x_1 :
            E)) ''
      Metric.closedBall 0 1)
calc_2 :
  norm (E := E)
      ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
              ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
            (a : E) → E)
          b :
        E) =
    ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖
⊢ ‖b⋆‖ * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖ ≤
    sSup
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)

Tactic:
calc
    _ ≤ ‖star x.fst • (x.fst • b + x.snd * b) + star x.snd * (x.fst • b + x.snd * b)‖ := by
      nth_rewrite 2 [← one_mul ‖_ + _‖]
      gcongr
      exact (norm_star b).symm ▸ mem_closedBall_zero_iff.1 hb
    _ ≤ sSup (_ '' Metric.closedBall 0 1) := le_csSup ?_ ⟨b, hb, ?_⟩

Premises used: HMul.hMul, Prod.fst, HAdd.hAdd, Unitization.toProd, Set.image, HSMul.hSMul, Metric.closedBall, OfNat.ofNat, Prod.snd, SupSet.sSup, Star.star
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
⊢ BddAbove (α := ℝ)
    ((fun (x_1 : E) ↦
        norm (E := E)
          ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                  ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                  ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                (a : E) → E)
              x_1 :
            E)) ''
      Metric.closedBall 0 1)

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

Premises used: Norm.norm, HMul.hMul, Prod.fst, BddAbove, Set.Nonempty, HAdd.hAdd, Unitization.toProd, Exists.intro, Prod.snd, Star.star
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
calc_1 :
  Membership.mem (γ := Set ℝ)
    (upperBounds
      ((fun (x_1 : E) ↦
          norm (E := E)
            ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                    ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1))
    (‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖)
⊢ BddAbove (α := ℝ)
    ((fun (x_1 : E) ↦
        norm (E := E)
          ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                  ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                  ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                (a : E) → E)
              x_1 :
            E)) ''
      Metric.closedBall 0 1)

Tactic:
refine ⟨‖(star x * x).fst‖ + ‖(star x * x).snd‖, ?_⟩
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
⊢ (fun (x_1 : E) ↦
        norm (E := E)
          ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                  ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                  ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                (a : E) → E)
              x_1 :
            E))
      y ≤
    ‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖

Tactic:
(norm_add_le _ _).trans ?_

Premises used: norm_add_le, LE.le.trans
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
calc_1 :
  norm (E := E)
        (((↑((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) +
      norm (E := E) (((↑((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖
⊢ (fun (x_1 : E) ↦
        norm (E := E)
          ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
                  ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
                  ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
                (a : E) → E)
              x_1 :
            E))
      y ≤
    ‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖

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

Premises used: norm_add_le, LE.le.trans
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
calc_1 :
  norm (E := E)
      (((↑((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖
calc_1₁ :
  norm (E := E) (((↑((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.2‖
⊢ norm (E := E)
        (((↑((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) +
      norm (E := E) (((↑((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖ + ‖(x⋆ * x).toProd.2‖

Tactic:
gcongr
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
calc_1 :
  norm (E := E) (((↑(HSMul.hSMul (β := E →L[𝕜] E) (x⋆ * x).toProd.1 1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖
⊢ norm (E := E)
      (((↑((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
⊢ norm (E := E) (((↑(HSMul.hSMul (β := E →L[𝕜] E) (x⋆ * x).toProd.1 1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖

Tactic:
(norm_smul _ _).trans_le ?_

Premises used: norm_smul, Eq.trans_le
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
calc_1 : ‖(x⋆ * x).toProd.1‖ * norm (E := E) (((↑1 : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤ ‖(x⋆ * x).toProd.1‖
⊢ norm (E := E) (((↑(HSMul.hSMul (β := E →L[𝕜] E) (x⋆ * x).toProd.1 1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖

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

Premises used: norm_smul, Eq.trans_le
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
⊢ ‖(x⋆ * x).toProd.1‖ * norm (E := E) (((↑1 : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤ ‖(x⋆ * x).toProd.1‖

Tactic:
simpa only [mul_one] using
        mul_le_mul_of_nonneg_left (mem_closedBall_zero_iff.1 hy) (norm_nonneg (star x * x).fst)

Premises used: HMul.hMul, Prod.fst, Unitization.toProd, Iff.mp, mul_one, mem_closedBall_zero_iff, mul_le_mul_of_nonneg_left, norm_nonneg, Star.star
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
⊢ norm (E := E) (((↑((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.2‖

Tactic:
(unit_le_opNorm _ y <| mem_closedBall_zero_iff.1 hy).trans (opNorm_mul_apply_le _ _ _)

Premises used: ContinuousLinearMap.opNorm_mul_apply_le, Iff.mp, ContinuousLinearMap.unit_le_opNorm, LE.le.trans, mem_closedBall_zero_iff
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
y : E
hy : Membership.mem (γ := Set E) (Metric.closedBall 0 1) y
⊢ norm (E := E) (((↑((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.2‖

Tactic:
exact (unit_le_opNorm _ y <| mem_closedBall_zero_iff.1 hy).trans (opNorm_mul_apply_le _ _ _)

Premises used: ContinuousLinearMap.opNorm_mul_apply_le, Iff.mp, ContinuousLinearMap.unit_le_opNorm, LE.le.trans, mem_closedBall_zero_iff
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
calc_2 :
  ‖(x.toProd.1⋆ * x.toProd.1) • b +
        (x.toProd.1⋆ • x.toProd.2 * b + x.toProd.1 • x.toProd.2⋆ * b + x.toProd.2⋆ * x.toProd.2 * b)‖ =
    ‖x.toProd.1⋆ • x.toProd.1 • b + x.toProd.1⋆ • (x.toProd.2 * b) +
        (x.toProd.2⋆ * x.toProd.1 • b + x.toProd.2⋆ * (x.toProd.2 * b))‖
⊢ norm (E := E)
      ((HAdd.hAdd (α := E →L[𝕜] E) (β := E →L[𝕜] E)
              ((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1 : E →L[𝕜] E)
              ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E) :
            (a : E) → E)
          b :
        E) =
    ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖

Tactic:
simp only [ContinuousLinearMap.add_apply, mul_apply', Unitization.snd_star, Unitization.snd_mul,
      Unitization.fst_mul, Unitization.fst_star, Algebra.algebraMap_eq_smul_one, smul_apply,
      one_apply, smul_add, mul_add, add_mul]

Premises used: add_mul, ContinuousLinearMap.smul_apply, Unitization.snd_mul, Unitization.fst_mul, ContinuousLinearMap.add_apply, ContinuousLinearMap.one_apply, Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.mul_apply', Unitization.snd_star, mul_add, Unitization.fst_star, smul_add
-- 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
x : Unitization 𝕜 E
b : E
hb : Membership.mem (γ := Set E) (Metric.closedBall 0 1) b
⊢ ‖(x.toProd.1⋆ * x.toProd.1) • b +
        (x.toProd.1⋆ • x.toProd.2 * b + x.toProd.1 • x.toProd.2⋆ * b + x.toProd.2⋆ * x.toProd.2 * b)‖ =
    ‖x.toProd.1⋆ • x.toProd.1 • b + x.toProd.1⋆ • (x.toProd.2 * b) +
        (x.toProd.2⋆ * x.toProd.1 • b + x.toProd.2⋆ * (x.toProd.2 * b))‖

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

Premises used: add_assoc, mul_assoc, smul_smul, smul_mul_assoc, mul_smul_comm