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
inst_9 : CStarRing 𝕜
x : Unitization 𝕜 E
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)
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
simp only [Unitization.norm_def, Prod.norm_def]

Premises used: Prod.norm_def, Unitization.norm_def
-- 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
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)‖
⊢ ∀ (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

Tactic:
simp only [Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_star]

Premises used: Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_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
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)‖
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)‖
⊢ ‖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

Premises used: Algebra.algebraMap, Prod.fst, ContinuousLinearMap, ContinuousLinearMap.mul, Unitization.toProd, RingHom.id, Prod.snd, DFunLike.coe
-- 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_1 x : Unitization 𝕜 E
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
pos :
  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)‖

Tactic:
simp only [h, norm_zero]

Premises used: norm_zero
-- 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_1 x : Unitization 𝕜 E
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
⊢ 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)‖

Tactic:
norm_nonneg _

Premises used: 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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
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
⊢ 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)‖

Tactic:
exact norm_nonneg _

Premises used: 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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
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
rw :
  ‖HMul.hMul (α := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
        ((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⋆ * 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

Tactic:
rw [map_mul, Prod.snd_mul]

Premises used: Prod.snd_mul, map_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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
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
⊢ ‖HMul.hMul (α := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
        ((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

Tactic:
norm_mul_le _ _

Premises used: 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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
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
⊢ ‖HMul.hMul (α := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x⋆).2
        ((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

Tactic:
exact norm_mul_le _ _

Premises used: 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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
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
⊢ HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 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

Tactic:
have : ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤
          ‖(Unitization.splitMul 𝕜 E (star x)).snd‖ * ‖(Unitization.splitMul 𝕜 E x).snd‖ :=
          (norm_splitMul_snd_sq 𝕜 x).trans <| by
            rw [map_mul, Prod.snd_mul]
            exact 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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
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
this :
  HPow.hPow (β := ℕ) (norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) x).2) 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 *
      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

Tactic:
rw [sq] at this

Premises used: sq
-- 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_1 x : Unitization 𝕜 E
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
this :
  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
⊢ 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)‖

Tactic:
rw [← Ne, ← norm_pos_iff] at h

Premises used: norm_pos_iff, Ne
-- 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_1 x : Unitization 𝕜 E
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
this :
  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
h₁ :
  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)‖
⊢ 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

Tactic:
rw [← Ne, ← norm_pos_iff] at h

Premises used: norm_pos_iff, Ne
-- 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_1 x : Unitization 𝕜 E
h :
  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)‖
this :
  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
⊢ ‖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)‖

Tactic:
simp only [Unitization.splitMul_apply, Unitization.snd_star,
          Unitization.fst_star] at this

Premises used: Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_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
inst_9 : CStarRing 𝕜
x_1 x : Unitization 𝕜 E
h :
  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)‖
this :
  ‖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)‖
⊢ ‖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:
(mul_le_mul_iff_left₀ h).mp this

Premises used: Iff.mp, mul_le_mul_iff_left₀
-- 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_1 x : Unitization 𝕜 E
h :
  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)‖
this :
  ‖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)‖
⊢ ‖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:
exact (mul_le_mul_iff_left₀ h).mp this

Premises used: Iff.mp, mul_le_mul_iff_left₀
-- 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
⊢ ∀ (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

Tactic:
have h₁ : ∀ x : Unitization 𝕜 E,
        ‖(Unitization.splitMul 𝕜 E x).snd‖ ≤ ‖(Unitization.splitMul 𝕜 E (star x)).snd‖ := by
      simp only [Unitization.splitMul_apply, Unitization.snd_star, Unitization.fst_star]
      intro x
      /- split based on whether the term inside the norm is zero or not. If so, it's trivial.
      If not, then apply `norm_splitMul_snd_sq` and cancel one copy of the norm -/
      by_cases h : algebraMap 𝕜 (E →L[𝕜] E) x.fst + mul 𝕜 E x.snd = 0
      · simp only [h, norm_zero]
        exact norm_nonneg _
      · have : ‖(Unitization.splitMul 𝕜 E x).snd‖ ^ 2 ≤
          ‖(Unitization.splitMul 𝕜 E (star x)).snd‖ * ‖(Unitization.splitMul 𝕜 E x).snd‖ :=
          (norm_splitMul_snd_sq 𝕜 x).trans <| by
            rw [map_mul, Prod.snd_mul]
            exact norm_mul_le _ _
        rw [sq] at this
        rw [← Ne, ← norm_pos_iff] at h
        simp only [Unitization.splitMul_apply, Unitization.snd_star,
          Unitization.fst_star] at this
        exact (mul_le_mul_iff_left₀ h).mp this
-- 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
⊢ 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

Tactic:
le_antisymm ?_ (norm_splitMul_snd_sq 𝕜 x)

Premises used: le_antisymm, Unitization.norm_splitMul_snd_sq