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)
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)
hx' : ‖x‖₊ ≤ 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:
⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), ?_⟩

Premises used: Iff.mpr, nnnorm_star, Eq.trans_le, And.intro, Exists.intro, mem_closedBall_zero_iff, 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)
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)
hx' : ‖x‖₊ ≤ 1
refine_2 :
  r <
    sSup
      ((fun (a_1 : A) ↦
          ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
              a_1‖₊) ''
        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:
refine ⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), ?_⟩
-- 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)
hx' : ‖x‖₊ ≤ 1
⊢ r <
    sSup
      ((fun (a_1 : A) ↦
          ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
              a_1‖₊) ''
        Metric.closedBall 0 1)

Tactic:
lt_csSup_of_lt ?_ ⟨x, hx, rfl⟩ ?_

Premises used: And.intro, Exists.intro, lt_csSup_of_lt, 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)
hx' : ‖x‖₊ ≤ 1
refine_2 :
  BddAbove (α := ℝ≥0)
    ((fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
            a_1‖₊) ''
      Metric.closedBall 0 1)
refine_2₁ :
  r <
    (fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
            a_1‖₊)
      x
⊢ r <
    sSup
      ((fun (a_1 : A) ↦
          ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
              a_1‖₊) ''
        Metric.closedBall 0 1)

Tactic:
refine lt_csSup_of_lt ?_ ⟨x, hx, 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)
hx' : ‖x‖₊ ≤ 1
⊢ BddAbove (α := ℝ≥0)
    ((fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
            a_1‖₊) ''
      Metric.closedBall 0 1)

Tactic:
⟨‖a‖₊ * ‖a‖₊, ?_⟩

Premises used: HMul.hMul, NNNorm.nnnorm, BddAbove, Set.Nonempty, Exists.intro
-- 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)
hx' : ‖x‖₊ ≤ 1
refine_2 :
  Membership.mem (γ := Set ℝ≥0)
    (upperBounds
      ((fun (a_1 : A) ↦
          ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
              a_1‖₊) ''
        Metric.closedBall 0 1))
    (‖a‖₊ * ‖a‖₊)
⊢ BddAbove (α := ℝ≥0)
    ((fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
            a_1‖₊) ''
      Metric.closedBall 0 1)

Tactic:
refine ⟨‖a‖₊ * ‖a‖₊, ?_⟩
-- 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)
hx' : ‖x‖₊ ≤ 1
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 (star x))) : A) : A)
            a_1‖₊)
      y ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
key (star x) y ((nnnorm_star x).trans_le hx') (mem_closedBall_zero_iff.1 hy)

Premises used: nnnorm_star, Eq.trans_le, Iff.mp, mem_closedBall_zero_iff, 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)
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)
hx' : ‖x‖₊ ≤ 1
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 (star x))) : A) : A)
            a_1‖₊)
      y ≤
    ‖a‖₊ * ‖a‖₊

Tactic:
exact key (star x) y ((nnnorm_star x).trans_le hx') (mem_closedBall_zero_iff.1 hy)

Premises used: nnnorm_star, Eq.trans_le, Iff.mp, mem_closedBall_zero_iff, 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)
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)
hx' : ‖x‖₊ ≤ 1
⊢ r <
    (fun (a_1 : A) ↦
        ‖HMul.hMul (α := A) ((a.toProd.2 : (a : A) → A) (star ((a.toProd.1 : (a : A) → A) (star (star x))) : A) : A)
            a_1‖₊)
      x

Tactic:
simpa only [a.central, star_star, CStarRing.nnnorm_star_mul_self, NNReal.sq_sqrt, ← sq]
            using pow_lt_pow_left₀ hxr zero_le' two_ne_zero

Premises used: star_star, DoubleCentralizer.central, sq, two_ne_zero, zero_le', pow_lt_pow_left₀, CStarRing.nnnorm_star_mul_self, NNReal.sq_sqrt
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalRing A₁
inst_1 : Module ℂ A₁
inst_2 : SMulCommClass ℝ A₁ A₁
inst_3 : IsScalarTower ℝ A₁ A₁
inst_4 : StarRing A₁
inst_5 : TopologicalSpace A₁
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A₁ IsSelfAdjoint
inst_7 : PartialOrder A₁
inst_8 : StarOrderedRing A₁
inst_9 : NonUnitalRing A₂
inst_10 : Module ℂ A₂
inst_11 : StarRing A₂
inst_12 : PartialOrder A₂
inst_13 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
a : A₁
ha : IsSelfAdjoint a
rw : IsSelfAdjoint.{u_2} (R := A₂) ((f : (a : A₁) → A₂) (a⁺ - a⁻) : A₂)
⊢ IsSelfAdjoint.{u_2} (R := A₂) ((f : (a : A₁) → A₂) a : A₂)

Tactic:
rw [← CFC.posPart_sub_negPart a ha]

Premises used: CFC.posPart_sub_negPart
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalRing A₁
inst_1 : Module ℂ A₁
inst_2 : SMulCommClass ℝ A₁ A₁
inst_3 : IsScalarTower ℝ A₁ A₁
inst_4 : StarRing A₁
inst_5 : TopologicalSpace A₁
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A₁ IsSelfAdjoint
inst_7 : PartialOrder A₁
inst_8 : StarOrderedRing A₁
inst_9 : NonUnitalRing A₂
inst_10 : Module ℂ A₂
inst_11 : StarRing A₂
inst_12 : PartialOrder A₂
inst_13 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
a : A₁
ha : IsSelfAdjoint a
⊢ IsSelfAdjoint.{u_2} (R := A₂) ((f : (a : A₁) → A₂) (a⁺ - a⁻) : A₂)

Tactic:
cfc_tac
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : IsSelfAdjoint x
a : x ≤ (algebraMap ℝ B₁ : (a : ℝ) → B₁) ‖x‖
⊢ LE.le.{u_4} (α := B₂) ((f : (a : B₁) → B₂) x : B₂)
    ((f : (a : B₁) → B₂) ((algebraMap ℝ B₁ : (a : ℝ) → B₁) ‖x‖ : B₁) : B₂)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : IsSelfAdjoint x
⊢ x ≤ (algebraMap ℝ B₁ : (a : ℝ) → B₁) ‖x‖

Tactic:
IsSelfAdjoint.le_algebraMap_norm_self hx

Premises used: IsSelfAdjoint.le_algebraMap_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : IsSelfAdjoint x
⊢ x ≤ (algebraMap ℝ B₁ : (a : ℝ) → B₁) ‖x‖

Tactic:
exact IsSelfAdjoint.le_algebraMap_norm_self hx

Premises used: IsSelfAdjoint.le_algebraMap_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ ‖‖x‖‖ = ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ ‖‖x‖‖ = ‖x‖

Tactic:
have h : ‖‖x‖‖ = ‖x‖ := by simp
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
h : ‖‖x‖‖ = ‖x‖
rw : norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) x : B₂) ≤ ‖HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)‖
⊢ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) x : B₂) ≤ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) 1 : B₂) * ‖x‖

Tactic:
rw [mul_comm, ← h, ← norm_smul ‖x‖ (f 1)]

Premises used: Norm.norm, norm_smul, mul_comm, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) x : B₂) ≤ ‖HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)‖

Tactic:
CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg hx) ?_

Premises used: PositiveLinearMap.map_nonneg, CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
refine : (f : (a : B₁) → B₂) x ≤ HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)
⊢ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) x : B₂) ≤ ‖HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)‖

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg hx) ?_

Premises used: PositiveLinearMap.map_nonneg, CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
rw : LE.le.{u_4} (α := B₂) ((f : (a : B₁) → B₂) x : B₂) ((f : (a : B₁) → B₂) (HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1) : B₂)
⊢ (f : (a : B₁) → B₂) x ≤ HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)

Tactic:
rw [← Complex.coe_smul, ← LinearMapClass.map_smul f]

Premises used: LinearMapClass.map_smul, Complex.coe_smul
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
a : x ≤ HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1
⊢ LE.le.{u_4} (α := B₂) ((f : (a : B₁) → B₂) x : B₂) ((f : (a : B₁) → B₂) (HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1) : B₂)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
a : x ≤ (algebraMap ℂ B₁ : (a : ℂ) → B₁) (↑‖x‖ : ℂ)
⊢ x ≤ HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1

Tactic:
rw [← Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ x ≤ (algebraMap ℂ B₁ : (a : ℂ) → B₁) (↑‖x‖ : ℂ)

Tactic:
IsSelfAdjoint.le_algebraMap_norm_self <| .of_nonneg hx

Premises used: IsSelfAdjoint.of_nonneg, IsSelfAdjoint.le_algebraMap_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
B₁ : Type u_3
B₂ : Type u_4
inst : CStarAlgebra B₁
inst_1 : CStarAlgebra B₂
inst_2 : PartialOrder B₁
inst_3 : PartialOrder B₂
inst_4 : StarOrderedRing B₁
inst_5 : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ x ≤ (algebraMap ℂ B₁ : (a : ℂ) → B₁) (↑‖x‖ : ℂ)

Tactic:
exact IsSelfAdjoint.le_algebraMap_norm_self <| .of_nonneg hx

Premises used: IsSelfAdjoint.le_algebraMap_norm_self
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
h_nonneg : ∃ (C : ℝ≥0), ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
obtain :
  ∀ (C : ℝ≥0) (hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖),
    ∃ (C : ℝ≥0), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖

Tactic:
obtain ⟨C, hmain⟩ := h_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖

Tactic:
⟨4 * C, fun x ↦ ?_⟩

Premises used: HMul.hMul, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
refine : ∀ (x : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖

Tactic:
refine ⟨4 * C, fun x ↦ ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
x : A₁
obtain :
  ∀ (y : Fin 4 → A₁) (hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i) (hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖)
    (hy : x = ∑ i : Fin 4, I ^ (↑i : ℕ) • y i), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖

Tactic:
obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x

Premises used: CStarAlgebra.exists_sum_four_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i : Fin 4, I ^ (↑i : ℕ) • y i
rw : norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑ i : Fin 4, I ^ (↑i : ℕ) • y i) : A₂)
| norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)

Tactic:
rw [hy]