awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖₊
have 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‖₊
Tactic: refine csSup_le (hball.image _) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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‖₊
⊢ ∃ (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
have 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)
Tactic: simp only [Set.mem_image, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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‖₊
⊢ ∃ (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)
have hr' : (sqrt : (a : ℝ≥0) → ℝ≥0) r < ‖a‖₊
Tactic: have hr' : NNReal.sqrt r < ‖a‖₊ := ‖a‖₊.sqrt_mul_self ▸ NNReal.sqrt_lt_sqrt.2 hr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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‖₊
⊢ ∃ (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)
have 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)
Tactic: simp_rw [← nnnorm_fst, ← sSup_unitClosedBall_eq_nnnorm] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨_, ⟨x, hx, rfl⟩, hxr⟩ := exists_lt_of_lt_csSup (hball.image _) hr'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (hypothesis)
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)
⊢ ∃ (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)
have hx' : ‖x‖₊ ≤ 1
Tactic: have hx' : ‖x‖₊ ≤ 1 := mem_closedBall_zero_iff.1 hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
have 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)
Tactic: refine ⟨star x, mem_closedBall_zero_iff.2 ((nnnorm_star x).trans_le hx'), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
have 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)
Tactic: refine lt_csSup_of_lt ?_ ⟨x, hx, rfl⟩ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
⊢ 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)
have 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
Tactic: refine lt_csSup_of_lt ?_ ⟨x, hx, rfl⟩ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Multiplier (goal)
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)
have 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‖₊)
Tactic: refine ⟨‖a‖₊ * ‖a‖₊, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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₂)
have rw : IsSelfAdjoint.{u_2} (R := A₂) ((f : (a : A₁) → A₂) (a⁺ - a⁻) : A₂)
Tactic: rw [← CFC.posPart_sub_negPart a ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
⊢ LE.le.{u_4} (α := B₂) ((f : (a : B₁) → B₂) x : B₂)
    ((f : (a : B₁) → B₂) ((algebraMap ℝ B₁ : (a : ℝ) → B₁) ‖x‖ : B₁) : B₂)
have a : x ≤ (algebraMap ℝ B₁ : (a : ℝ) → B₁) ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (hypothesis)
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₂) ≤ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) 1 : B₂) * ‖x‖
have h : ‖‖x‖‖ = ‖x‖
Tactic: have h : ‖‖x‖‖ = ‖x‖ := by simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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‖
⊢ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) x : B₂) ≤ norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) 1 : B₂) * ‖x‖
have rw : norm.{u_4} (E := B₂) ((f : (a : B₁) → B₂) x : B₂) ≤ ‖HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)‖
Tactic: rw [mul_comm, ← h, ← norm_smul ‖x‖ (f 1)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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₂)‖
have refine : (f : (a : B₁) → B₂) x ≤ HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)
Tactic: refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg hx) ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
⊢ (f : (a : B₁) → B₂) x ≤ HSMul.hSMul (β := B₂) ‖x‖ ((f : (a : B₁) → B₂) 1 : B₂)
have rw : LE.le.{u_4} (α := B₂) ((f : (a : B₁) → B₂) x : B₂) ((f : (a : B₁) → B₂) (HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1) : B₂)
Tactic: rw [← Complex.coe_smul, ← LinearMapClass.map_smul f]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
⊢ LE.le.{u_4} (α := B₂) ((f : (a : B₁) → B₂) x : B₂) ((f : (a : B₁) → B₂) (HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1) : B₂)
have a : x ≤ HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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 ≤ HSMul.hSMul (β := B₁) (↑‖x‖ : ℂ) 1
have a : x ≤ (algebraMap ℂ B₁ : (a : ℂ) → B₁) (↑‖x‖ : ℂ)
Tactic: rw [← Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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‖
⊢ ∃ (C : ℝ≥0), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
have 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‖
Tactic: obtain ⟨C, hmain⟩ := h_nonneg
Cleared hypotheses: h_nonneg
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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‖
have refine : ∀ (x : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
Tactic: refine ⟨4 * C, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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₁
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
have 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‖
Tactic: obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
| norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂)
have rw : norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑ i : Fin 4, I ^ (↑i : ℕ) • y i) : A₂)
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) x : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
have conv_lhs : norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑ i : Fin 4, I ^ (↑i : ℕ) • y i) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
Tactic: conv_lhs => rw [hy]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑ i : Fin 4, I ^ (↑i : ℕ) • y i) : A₂) ≤ (↑(4 * C) : ℝ) * ‖x‖
have simp : norm.{u_2} (E := A₂) (∑ x : Fin 4, HSMul.hSMul (β := A₂) (I ^ (↑x : ℕ)) ((f : (a : A₁) → A₂) (y x) : A₂)) ≤
  (↑(4 * C) : ℝ) * ‖x‖
Tactic: simp only [map_sum, map_smul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.PositiveLinearMap (goal)
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
⊢ norm.{u_2} (E := A₂) (∑ x : Fin 4, HSMul.hSMul (β := A₂) (I ^ (↑x : ℕ)) ((f : (a : A₁) → A₂) (y x) : A₂)) ≤
    (↑(4 * C) : ℝ) * ‖x‖
have apply : ∑ i : Fin 4, ‖HSMul.hSMul (β := A₂) (I ^ (↑i : ℕ)) ((f : (a : A₁) → A₂) (y i) : A₂)‖ ≤ (↑(4 * C) : ℝ) * ‖x‖
Tactic: apply norm_sum_le _ _ |>.trans