awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ 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.toProd.1 : E →L[𝕜] E)
                    ((mul 𝕜 E : (a : E) → E →L[𝕜] E) x.toProd.2 : E →L[𝕜] E) :
                  (a : E) → E)
                x_1 :
              E)) ''
        Metric.closedBall 0 1) ≤
    √‖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)‖
have refine : ∀ (b : ℝ),
  Membership.mem (γ := Set ℝ)
      ((fun (x_1 : E) ↦
          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)
                x_1 :
              E)) ''
        Metric.closedBall 0 1)
      b →
    b ≤
      √‖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: refine csSup_le ((Metric.nonempty_closedBall.2 zero_le_one).image _) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ 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)‖
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)
have 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)
Tactic: refine (norm_mul_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)‖ ≤
    ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖
have 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)‖
Tactic: nth_rewrite 2 [← one_mul ‖_ + _‖]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)‖ ≤
    1 * ‖x.toProd.1⋆ • (x.toProd.1 • b + x.toProd.2 * b) + x.toProd.2⋆ * (x.toProd.1 • b + x.toProd.2 * b)‖
have hbc : ‖b⋆‖ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)
have 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)
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, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)
⊢ ‖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)
have 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)‖
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, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)
have 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‖)
Tactic: refine ⟨‖(star x * x).fst‖ + ‖(star x * x).snd‖, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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‖
have 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‖
Tactic: refine (norm_add_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)
        (((↑((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‖
have 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‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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‖
⊢ 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‖
have 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‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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)
      (((↑((algebraMap 𝕜 (E →L[𝕜] E) : (a : 𝕜) → E →L[𝕜] E) (x⋆ * x).toProd.1) : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤
    ‖(x⋆ * x).toProd.1‖
have 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‖
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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‖
have calc_1 : ‖(x⋆ * x).toProd.1‖ * norm (E := E) (((↑1 : E →ₗ[𝕜] E) : (a : E) → E) y : E) ≤ ‖(x⋆ * x).toProd.1‖
Tactic: refine (norm_smul _ _).trans_le ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ 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)‖
have 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))‖
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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖
have simp : 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⋆ * x)).1)
    (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2)
Tactic: simp only [Unitization.norm_def, Prod.norm_def]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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
⊢ ∀ (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
have simp : ∀ (x : Unitization 𝕜 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)‖ ≤
    ‖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)‖
Tactic: simp only [Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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_1 x : Unitization 𝕜 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)‖ ≤
    ‖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)‖
have pos : ∀
  (h :
    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) =
      0),
  ‖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)‖ ≤
    ‖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)‖
Tactic: by_cases h : algebraMap 𝕜 (E →L[𝕜] E) x.fst + mul 𝕜 E x.snd = 0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Unitization (goal)
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_1 x : Unitization 𝕜 E
pos :
  ∀
    (h :
      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) =
        0),
    ‖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)‖ ≤
      ‖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)‖
⊢ ‖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)‖ ≤
    ‖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)‖
have neg : ∀
  (h :
    ¬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) =
        0),
  ‖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)‖ ≤
    ‖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)‖
Tactic: by_cases h : algebraMap 𝕜 (E →L[𝕜] E) x.fst + mul 𝕜 E x.snd = 0