awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a : E
⊢ norm (E := E →L[𝕜] E) ((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)

Tactic:
opNorm_le_bound _ (norm_nonneg _) fun b => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a : E
refine :
  ∀ (b : E),
    norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) ≤
      norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖
⊢ norm (E := E →L[𝕜] E) ((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E)

Tactic:
refine opNorm_le_bound _ (norm_nonneg _) fun b => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a b : E
⊢ norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) =
    norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E)

Tactic:
simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)

Premises used: norm_star, HMul.hMul, star_star, ContinuousLinearMap.flip_apply, ContinuousLinearMap.mul_apply', StarMul.star_mul, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a b : E
⊢ norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖

Tactic:
simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)

Premises used: norm_star, ContinuousLinearMap.le_opNorm, ContinuousLinearMap.flip_apply, ContinuousLinearMap.mul, ContinuousLinearMap.mul_apply', ContinuousLinearMap.flip, DFunLike.coe, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a b : E
calc :
  norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) =
    norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E)
calc₁ :
  norm (E := E) ((((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) b⋆ : E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖
⊢ norm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a⋆ : E →L[𝕜] E) : (a : E) → E) b : E) ≤
    norm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) * ‖b‖

Tactic:
calc ‖mul 𝕜 E (star a) b‖ = ‖(mul 𝕜 E).flip a (star b)‖ := by
        simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)
    _ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖ := by
        simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)

Premises used: ContinuousLinearMap.mul, ContinuousLinearMap.flip, DFunLike.coe, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
a : E
⊢ nnnorm (E := E →L[𝕜] E) ((flip (mul 𝕜 E) : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) = ‖a‖₊

Tactic:
Subtype.ext (opNorm_mul_flip_apply 𝕜 a)

Premises used: ContinuousLinearMap.opNorm_mul_flip_apply, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.CStarAlgebra.Unitization
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NonUnitalNormedRing E
inst_2 : StarRing E
inst_3 : NormedStarGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower 𝕜 E E
inst_6 : SMulCommClass 𝕜 E E
inst_7 : RegularNormedAlgebra 𝕜 E
⊢ Isometry.{u_2, u_2} (α := E) (β := E →L[𝕜] E) (⇑(flip (mul 𝕜 E)) : (a : E) → E →L[𝕜] E)

Tactic:
AddMonoidHomClass.isometry_of_norm _ (opNorm_mul_flip_apply 𝕜)

Premises used: AddMonoidHomClass.isometry_of_norm, ContinuousLinearMap.opNorm_mul_flip_apply
-- 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
a : E
rw :
  sSup
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊
⊢ nnnorm (E := E →L[𝕜] E) ((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) = ‖a‖₊

Tactic:
rw [← sSup_unitClosedBall_eq_nnnorm]

Premises used: ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm
-- 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
a : E
⊢ sSup
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_

Premises used: csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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
a : E
refine_1 :
  Set.Nonempty (α := NNReal)
    ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
      Metric.closedBall 0 1)
refine_2 :
  ∀ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 →
      a_1 ≤ ‖a‖₊
refine_3 :
  ∀ (r : NNReal) (hr : r < ‖a‖₊),
    ∃ (a_1 : NNReal),
      Membership.mem (γ := Set NNReal)
          ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
            Metric.closedBall 0 1)
          a_1 ∧
        r < a_1
⊢ sSup
      ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt ?_ ?_ fun r hr => ?_

Premises used: csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- 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
a : E
⊢ Set.Nonempty (α := NNReal)
    ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
      Metric.closedBall 0 1)

Tactic:
(Metric.nonempty_closedBall.mpr zero_le_one).image _

Premises used: Iff.mpr, zero_le_one, Metric.nonempty_closedBall, Set.Nonempty.image
-- 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
a : E
⊢ Set.Nonempty (α := NNReal)
    ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
      Metric.closedBall 0 1)

Tactic:
exact (Metric.nonempty_closedBall.mpr zero_le_one).image _

Premises used: Iff.mpr, zero_le_one, Metric.nonempty_closedBall, Set.Nonempty.image
-- 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
a x : E
hx : Membership.mem (γ := Set E) (Metric.closedBall 0 1) x
⊢ (fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) x ≤ ‖a‖₊

Tactic:
((mul 𝕜 E a).unit_le_opNorm x <| mem_closedBall_zero_iff.mp hx).trans
          (opNorm_mul_apply_le 𝕜 E a)

Premises used: ContinuousLinearMap.mul, ContinuousLinearMap.opNorm_mul_apply_le, Iff.mp, ContinuousLinearMap.unit_le_opNorm, LE.le.trans, mem_closedBall_zero_iff, 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
a x : E
hx : Membership.mem (γ := Set E) (Metric.closedBall 0 1) x
⊢ (fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) x ≤ ‖a‖₊

Tactic:
exact
        ((mul 𝕜 E a).unit_le_opNorm x <| mem_closedBall_zero_iff.mp hx).trans
          (opNorm_mul_apply_le 𝕜 E a)

Premises used: ContinuousLinearMap.mul, ContinuousLinearMap.opNorm_mul_apply_le, Iff.mp, ContinuousLinearMap.unit_le_opNorm, LE.le.trans, mem_closedBall_zero_iff, 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
a : E
r : NNReal
hr : r < ‖a‖₊
⊢ 0 < ‖a‖₊

Tactic:
have ha : 0 < ‖a‖₊ := zero_le'.trans_lt hr
-- 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
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
⊢ r * ‖a‖₊⁻¹ < 1

Tactic:
rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr

Premises used: NNNorm.nnnorm, LT.lt.ne', NNReal.lt_inv_iff_mul_lt, inv_inv, inv_ne_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
a : E
r : NNReal
hr : r < ‖a‖₊
ha : 0 < ‖a‖₊
hr₁ : r * ‖a‖₊⁻¹ < 1
⊢ 0 < ‖a‖₊

Tactic:
rw [← inv_inv ‖a‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero ha.ne')] at hr

Premises used: NNNorm.nnnorm, LT.lt.ne', NNReal.lt_inv_iff_mul_lt, inv_inv, inv_ne_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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
refine_3 :
  ∀ (k : 𝕜) (hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊) (hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹),
    ∃ (a_1 : NNReal),
      Membership.mem (γ := Set NNReal)
          ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
            Metric.closedBall 0 1)
          a_1 ∧
        r < a_1
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1

Tactic:
obtain ⟨k, hk₁, hk₂⟩ :=
        NormedField.exists_lt_nnnorm_lt 𝕜 (mul_lt_mul_of_pos_right hr <| inv_pos.2 ha)

Premises used: Iff.mpr, NormedField.exists_lt_nnnorm_lt, inv_pos, mul_lt_mul_of_pos_right
-- 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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1

Tactic:
⟨_, ⟨k • star a, ?_, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, HSMul.hSMul, rfl, 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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
refine_3 : Membership.mem (γ := Set E) (Metric.closedBall 0 1) (k • a⋆)
refine_3₁ :
  r < (fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) (k • a⋆)
⊢ ∃ (a_1 : NNReal),
    Membership.mem (γ := Set NNReal)
        ((fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1

Tactic:
refine ⟨_, ⟨k • star a, ?_, rfl⟩, ?_⟩
-- 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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (k • a⋆)

Tactic:
simpa only [mem_closedBall_zero_iff, norm_smul, one_mul, norm_star] using
          (NNReal.le_inv_iff_mul_le ha.ne').1 (one_mul ‖a‖₊⁻¹ ▸ hk₂.le : ‖k‖₊ ≤ ‖a‖₊⁻¹)

Premises used: norm_star, norm_smul, NNNorm.nnnorm, Eq.rec, LT.lt.le, LT.lt.ne', Inv.inv, NNReal.le_inv_iff_mul_le, Iff.mp, mem_closedBall_zero_iff, 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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
refine_3 : r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)
⊢ r < (fun (x : E) ↦ nnnorm (E := E) ((((mul 𝕜 E : (a : E) → E →L[𝕜] E) a : E →L[𝕜] E) : (a : E) → E) x : E)) (k • a⋆)

Tactic:
simp only [map_smul, nnnorm_smul, mul_apply', CStarRing.nnnorm_self_mul_star]

Premises used: nnnorm_smul, ContinuousLinearMap.mul_apply', CStarRing.nnnorm_self_mul_star, map_smul
-- 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
a : E
r : NNReal
hr : r * ‖a‖₊⁻¹ < 1
ha : 0 < ‖a‖₊
k : 𝕜
hk₁ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < 1 * ‖a‖₊⁻¹
refine_3 : r / (‖a‖₊ * ‖a‖₊) < ‖k‖₊
refine_3₁ : r * (‖a‖₊ * ‖a‖₊)⁻¹ < ‖k‖₊
refine_3₂ : r * (‖a‖₊⁻¹ * ‖a‖₊⁻¹) < ‖k‖₊
refine_3₃ refine_3₄ refine_3₅ refine_3₆ : r * ‖a‖₊⁻¹ * ‖a‖₊⁻¹ < ‖k‖₊
⊢ r < ‖k‖₊ * (‖a‖₊ * ‖a‖₊)

Tactic:
rwa [← div_lt_iff₀ (mul_pos ha ha), div_eq_mul_inv, mul_inv, ← mul_assoc]

Premises used: mul_inv, mul_assoc, div_lt_iff₀, div_eq_mul_inv, mul_pos
-- 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
⊢ 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⋆ * x)).2

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

Premises used: Real.le_sqrt, Iff.mp, 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
refine :
  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 ≤
    norm.{u_2} (E := E →L[𝕜] E) ((splitMul 𝕜 E : (a : Unitization 𝕜 E) → 𝕜 × (E →L[𝕜] E)) (x⋆ * x)).2

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

Premises used: Real.le_sqrt, Iff.mp, 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
simp :
  ‖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⋆ * x).toProd.1 : E →L[𝕜] E)
          ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * 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⋆ * x)).2)

Tactic:
simp only [Unitization.splitMul_apply]

Premises used: Unitization.splitMul_apply
-- 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
rw :
  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)‖
⊢ ‖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⋆ * x).toProd.1 : E →L[𝕜] E)
          ((mul 𝕜 E : (a : E) → E →L[𝕜] E) (x⋆ * x).toProd.2 : E →L[𝕜] E)‖

Tactic:
rw [← sSup_unitClosedBall_eq_norm]

Premises used: ContinuousLinearMap.sSup_unitClosedBall_eq_norm
-- 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
⊢ 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)‖

Tactic:
csSup_le ((Metric.nonempty_closedBall.2 zero_le_one).image _) ?_

Premises used: Iff.mpr, zero_le_one, Metric.nonempty_closedBall, Set.Nonempty.image, csSup_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
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)‖
⊢ 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)‖

Tactic:
refine csSup_le ((Metric.nonempty_closedBall.2 zero_le_one).image _) ?_

Premises used: Iff.mpr, zero_le_one, Metric.nonempty_closedBall, Set.Nonempty.image, csSup_le