awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
⊢ Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)

Tactic:
have hball : (Metric.closedBall (0 : A) 1).Nonempty :=
        Metric.nonempty_closedBall.2 zero_le_one
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
rw :
  ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) ((a.toProd.1 : (a : A) → A) y : A)‖₊ ≤
    ‖a‖₊ * ‖a‖₊
⊢ ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
rw [a.central]

Premises used: DoubleCentralizer.central
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) ((a.toProd.1 : (a : A) → A) y : A)‖₊ ≤
    nnnorm (E := A) ((a.toProd.1 : (a : A) → A) (star x) : A) * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) y : A)

Tactic:
nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _

Premises used: nnnorm_mul_le, nnnorm_star, Eq.rec, Prod.fst, DFunLike.coe, DoubleCentralizer.toProd, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) (star x) : A) * nnnorm (E := A) ((a.toProd.1 : (a : A) → A) y : A) ≤
    ‖a.toProd.1‖₊ * 1 * (‖a.toProd.1‖₊ * 1)

Tactic:
(mul_le_mul' (a.fst.le_opNorm_of_le ((nnnorm_star x).trans_le hx))
              (a.fst.le_opNorm_of_le hy))

Premises used: nnnorm_star, Eq.trans_le, ContinuousLinearMap.le_opNorm_of_le, Prod.fst, mul_le_mul', DoubleCentralizer.toProd
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖a.toProd.1‖₊ * 1 * (‖a.toProd.1‖₊ * 1) ≤ ‖a‖₊ * ‖a‖₊

Tactic:
simp only [mul_one, nnnorm_fst, le_rfl]

Premises used: le_rfl, DoubleCentralizer.nnnorm_fst, mul_one
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
nnnorm_star : ‖a.toProd.1‖₊ * 1 * (‖a.toProd.1‖₊ * 1) ≤ ‖a‖₊ * ‖a‖₊
⊢ ‖HMul.hMul (α := A) (β := A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) ((a.toProd.1 : (a : A) → A) y : A)‖₊ ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
calc
          ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
            nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
          _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
            (mul_le_mul' (a.fst.le_opNorm_of_le ((nnnorm_star x).trans_le hx))
              (a.fst.le_opNorm_of_le hy))
          _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]

Premises used: HMul.hMul, NNNorm.nnnorm, Prod.fst, OfNat.ofNat, DFunLike.coe, DoubleCentralizer.toProd, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
⊢ ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊

Tactic:
have key :
        ∀ x y, ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.snd (star (a.fst (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊ := by
        intro x y hx hy
        rw [a.central]
        calc
          ‖star (a.fst (star x)) * a.fst y‖₊ ≤ ‖a.fst (star x)‖₊ * ‖a.fst y‖₊ :=
            nnnorm_star (a.fst (star x)) ▸ nnnorm_mul_le _ _
          _ ≤ ‖a.fst‖₊ * 1 * (‖a.fst‖₊ * 1) :=
            (mul_le_mul' (a.fst.le_opNorm_of_le ((nnnorm_star x).trans_le hx))
              (a.fst.le_opNorm_of_le hy))
          _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
rw : ‖(star a * a).toProd.2‖₊ = ‖a‖₊ * ‖a‖₊
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊

Tactic:
rw [← nnnorm_snd]

Premises used: DoubleCentralizer.nnnorm_snd
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
simp :
  sSup
      ((fun (a_1 : A) ↦
          nnnorm (E := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
⊢ ‖(star a * a).toProd.2‖₊ = ‖a‖₊ * ‖a‖₊

Tactic:
simp only [mul_snd, ← sSup_unitClosedBall_eq_nnnorm, star_snd, mul_apply]

Premises used: DoubleCentralizer.star_snd, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, ContinuousLinearMap.mul_apply, DoubleCentralizer.mul_snd
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
simp :
  sSup
      ((fun (a_1 : A) ↦
          nnnorm (E := A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A)
                ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A) :
              A →L[𝕜] A)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          nnnorm (E := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊

Tactic:
simp only [← @opNNNorm_mul_apply 𝕜 _ A]

Premises used: ContinuousLinearMap.opNNNorm_mul_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
simp :
  sSup
      ((fun (a_1 : A) ↦
          sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          nnnorm (E := A →L[𝕜] A)
            ((mul 𝕜 A : (a : A) → A →L[𝕜] A)
                ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A) :
              A →L[𝕜] A)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊

Tactic:
simp only [← sSup_unitClosedBall_eq_nnnorm, mul_apply']

Premises used: ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, ContinuousLinearMap.mul_apply'
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
⊢ sSup
      ((fun (a_1 : A) ↦
          sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_

Premises used: Set.Nonempty.image, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
refine_1 :
  ∀ (a_1 : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
        ((fun (a_2 : A) ↦
            sSup
              ((fun (a_3 : A) ↦
                  ‖HMul.hMul (α := A)
                      ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_2)) : A) : A) a_3‖₊) ''
                Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1)
        a_1 →
      a_1 ≤ ‖a‖₊ * ‖a‖₊
refine_2 :
  ∀ (r : ℝ≥0) (hr : r < ‖a‖₊ * ‖a‖₊),
    ∃ (a_1 : ℝ≥0),
      Membership.mem (γ := Set ℝ≥0)
          ((fun (a_2 : A) ↦
              sSup
                ((fun (a_3 : A) ↦
                    ‖HMul.hMul (α := A)
                        ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_2)) : A) : A) a_3‖₊) ''
                  Metric.closedBall 0 1)) ''
            Metric.closedBall 0 1)
          a_1 ∧
        r < a_1
⊢ sSup
      ((fun (a_1 : A) ↦
          sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1)) ''
        Metric.closedBall 0 1) =
    ‖a‖₊ * ‖a‖₊

Tactic:
refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_

Premises used: Set.Nonempty.image, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
x : A
hx : Membership.mem (γ := Set A) (Metric.closedBall 0 1) x
⊢ (fun (a_1 : A) ↦
        (sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1) :
          ℝ≥0))
      x ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
csSup_le (hball.image _) ?_

Premises used: Set.Nonempty.image, csSup_le
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
x : A
hx : Membership.mem (γ := Set A) (Metric.closedBall 0 1) x
refine_1 :
  ∀ (b : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
        ((fun (a_1 : A) ↦
            ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A)
                a_1‖₊) ''
          Metric.closedBall 0 1)
        b →
      b ≤ ‖a‖₊ * ‖a‖₊
⊢ (fun (a_1 : A) ↦
        (sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1) :
          ℝ≥0))
      x ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
refine csSup_le (hball.image _) ?_

Premises used: Set.Nonempty.image, csSup_le
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
x : A
hx : Membership.mem (γ := Set A) (Metric.closedBall 0 1) x
y : A
hy : Membership.mem (γ := Set A) (Metric.closedBall 0 1) y
⊢ (fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) a_1‖₊)
      y ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
x : A
hx : Membership.mem (γ := Set A) (Metric.closedBall 0 1) x
y : A
hy : Membership.mem (γ := Set A) (Metric.closedBall 0 1) y
⊢ (fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) a_1‖₊)
      y ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
exact key x y (mem_closedBall_zero_iff.1 hx) (mem_closedBall_zero_iff.1 hy)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
refine_2 :
  ∃ (a_1 : A),
    Membership.mem (γ := Set A) (Metric.closedBall 0 1) a_1 ∧
      r <
        sSup
          ((fun (a_2 : A) ↦
              ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                  a_2‖₊) ''
            Metric.closedBall 0 1)
⊢ ∃ (a_1 : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
        ((fun (a_2 : A) ↦
            sSup
              ((fun (a_3 : A) ↦
                  ‖HMul.hMul (α := A)
                      ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_2)) : A) : A) a_3‖₊) ''
                Metric.closedBall 0 1)) ''
          Metric.closedBall 0 1)
        a_1 ∧
      r < a_1

Tactic:
simp only [Set.mem_image, exists_exists_and_eq_and]

Premises used: Set.mem_image, exists_exists_and_eq_and
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) r < ‖a‖₊

Tactic:
have hr' : NNReal.sqrt r < ‖a‖₊ := ‖a‖₊.sqrt_mul_self ▸ NNReal.sqrt_lt_sqrt.2 hr
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : (sqrt : (a : ℝ≥0) → ℝ≥0) r < ‖a‖₊
⊢ LT.lt (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
    (sSup ((fun (x : A) ↦ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) x : A)) '' Metric.closedBall 0 1) : ℝ≥0)

Tactic:
simp_rw [← nnnorm_fst, ← sSup_unitClosedBall_eq_nnnorm] at hr'

Premises used: ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, DoubleCentralizer.nnnorm_fst
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' :
  LT.lt (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
    (sSup ((fun (x : A) ↦ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) x : A)) '' Metric.closedBall 0 1) : ℝ≥0)
refine_2 :
  ∀ (x : A) (hx : Membership.mem (γ := Set A) (Metric.closedBall 0 1) x)
    (hxr :
      LT.lt (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
        ((fun (x : A) ↦ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) x : A)) x : ℝ≥0)),
    ∃ (a_1 : A),
      Membership.mem (γ := Set A) (Metric.closedBall 0 1) a_1 ∧
        r <
          sSup
            ((fun (a_2 : A) ↦
                ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                    a_2‖₊) ''
              Metric.closedBall 0 1)
⊢ ∃ (a_1 : A),
    Membership.mem (γ := Set A) (Metric.closedBall 0 1) a_1 ∧
      r <
        sSup
          ((fun (a_2 : A) ↦
              ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star a_1)) : A) : A)
                  a_2‖₊) ''
            Metric.closedBall 0 1)

Tactic:
obtain ⟨_, ⟨x, hx, rfl⟩, hxr⟩ := exists_lt_of_lt_csSup (hball.image _) hr'

Premises used: exists_lt_of_lt_csSup, Set.Nonempty.image, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Multiplier
Goal:
𝕜 : Type u_1
A : Type u_2
inst : DenselyNormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : StarRing A
inst_4 : CStarRing A
inst_5 : NormedSpace 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : Set.Nonempty.{u_2} (α := A) (Metric.closedBall 0 1)
key :
  ∀ (x y : A),
    ‖x‖₊ ≤ 1 →
      ‖y‖₊ ≤ 1 →
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star x)) : A) : A) y‖₊ ≤
          ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' :
  LT.lt (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
    (sSup ((fun (x : A) ↦ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) x : A)) '' Metric.closedBall 0 1) : ℝ≥0)
x : A
hx : Membership.mem (γ := Set A) (Metric.closedBall 0 1) x
hxr :
  LT.lt (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) r : ℝ≥0)
    ((fun (x : A) ↦ nnnorm (E := A) ((a.toProd.1 : (a : A) → A) x : A)) x : ℝ≥0)
⊢ ‖x‖₊ ≤ 1

Tactic:
have hx' : ‖x‖₊ ≤ 1 := mem_closedBall_zero_iff.1 hx