awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))) ≤
      ‖a‖
have h : LE.le.{u_2} (α := A) 0
  (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
      (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
      (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
      (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
    ((fun (i : Fin 4) ↦ i) ⟨2, sorry⟩))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩))
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨2, ⋯⟩ : Fin 4))) ≤
      ‖a‖
have h₁ : norm.{u_2} (E := A)
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) (⟨2, sorry⟩ : Fin 4))) ≤
  ‖a‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨2, ⋯⟩))
have h : LE.le.{u_2} (α := A) 0 (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))) ≤
      ‖a‖
have h : LE.le.{u_2} (α := A) 0
  (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
      (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
      (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
      (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
    ((fun (i : Fin 4) ↦ i) ⟨3, sorry⟩))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
h :
  LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩))
⊢ LE.le.{u_2} (α := A) 0
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩)) ∧
    norm.{u_2} (E := A)
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          ((fun (i : Fin 4) ↦ i) (⟨3, ⋯⟩ : Fin 4))) ≤
      ‖a‖
have h₁ : norm.{u_2} (E := A)
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) (⟨3, sorry⟩ : Fin 4))) ≤
  ‖a‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ LE.le.{u_2} (α := A) 0
    (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
        (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
      ((fun (i : Fin 4) ↦ i) ⟨3, ⋯⟩))
have h : LE.le.{u_2} (α := A) 0 (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ a =
    ∑ i : Fin 4,
      HSMul.hSMul (β := A) (I ^ (↑i : ℕ))
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          i)
have h : HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
      (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
    (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
      HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
  ∑ i : Fin 4,
    HSMul.hSMul (β := A) (I ^ (↑i : ℕ))
      (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
        i)
Tactic: nth_rw 1 [← CStarAlgebra.linear_combination_nonneg a]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart (goal)
Goal:
A : Type u_2
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
⊢ HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
      (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
        HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
    ∑ i : Fin 4,
      HSMul.hSMul (β := A) (I ^ (↑i : ℕ))
        (![(↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺,
            (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻,
            (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻]
          i)
have h : HSub.hSub (α := A) (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺
      (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
    (HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ -
      HSMul.hSMul (β := A) I (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻) =
  HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) I 0)
          (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ +
        HSMul.hSMul (β := A) (HPow.hPow (β := ℕ) I 1)
          (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁺ +
      HSMul.hSMul (α := ℂ) (β := A) (-1)
        (↑(((realPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻ +
    HSMul.hSMul (β := A) (-I) (↑(((imaginaryPart : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)⁻
Tactic: simp only [Fin.sum_univ_four, Fin.coe_ofNat_eq_mod, Matrix.cons_val, Nat.reduceMod, I_sq,
      I_pow_three]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
⊢ σ 𝕜 (↑u : E) ⊆ Metric.sphere 0 1
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
⊢ σ 𝕜 (↑u : E) ⊆ Metric.sphere 0 1
have refine_1 : ∀ (k : 𝕜) (hk : k ∈ σ 𝕜 (↑u : E)), ‖k‖ ≤ 1
Tactic: refine fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
refine_1 : ∀ (k : 𝕜) (hk : k ∈ σ 𝕜 (↑u : E)), ‖k‖ ≤ 1
⊢ σ 𝕜 (↑u : E) ⊆ Metric.sphere 0 1
have refine_2 : ∀ (k : 𝕜) (hk : k ∈ σ 𝕜 (↑u : E)), 1 ≤ ‖k‖
Tactic: refine fun k hk => mem_sphere_zero_iff_norm.mpr (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 (↑u : E)
⊢ 1 ≤ ‖k‖
have hk₁ : k ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u) : E)
Tactic: rw [← Unitary.val_toUnits_apply u] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u) : E)
⊢ 1 ≤ ‖k‖
have hnk : k ≠ 0
Tactic: have hnk := ne_zero_of_mem_of_unit hk
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u) : E)
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
have hk₁ : k⁻¹ ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)
Tactic: rw [← inv_inv (Unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk
Cleared hypotheses: hk, hnk
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : NormedRing E
inst_2 : StarRing E
inst_3 : CStarRing E
inst_4 : NormedAlgebra 𝕜 E
inst_5 : CompleteSpace E
u : ↥(unitary E)
h : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)
hnk : k ≠ 0
⊢ 1 ≤ ‖k‖
have this : ‖k‖⁻¹ ≤ norm.{u_2} (E := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)
Tactic: have : ‖k‖⁻¹ ≤ ‖(↑(Unitary.toUnits u)⁻¹ : E)‖ := by
      simpa only [norm_inv] using norm_le_norm_of_mem hk
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ quasispectrum ℝ≥0 a
⊢ x ≤ ‖a‖₊
have hx₁ : x ∈ σ ℝ≥0 (A := Unitization ℂ A) (↑a : Unitization ℂ A)
Tactic: rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ spectralRadius ℂ a = (↑‖a‖₊ : ℝ≥0∞)
have hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
Tactic: have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
⊢ spectralRadius ℂ a = (↑‖a‖₊ : ℝ≥0∞)
have refine : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (spectralRadius ℂ a))
Tactic: refine tendsto_nhds_unique ?_ hconst
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
⊢ Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (spectralRadius ℂ a))
have h : Eq (α := ℕ → ℝ≥0∞) (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞))
  ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n)
Tactic: convert!
    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞))
    ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n)
have h : ∀ (n : ℕ),
  (↑‖a‖₊ : ℝ≥0∞) =
    ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) n
Tactic: refine funext fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
n : ℕ
⊢ (↑‖a‖₊ : ℝ≥0∞) =
    ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) n
have h : (↑‖a‖₊ : ℝ≥0∞) =
  (↑‖a‖₊ : ℝ≥0∞) ^ ((↑(HPow.hPow (α := ℕ) 2 n) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (α := ℕ) 2 n) : ℝ))
Tactic: rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ spectralRadius ℂ a = (↑‖a‖₊ : ℝ≥0∞)
have refine : HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2
Tactic: refine (ENNReal.pow_right_strictMono two_ne_zero).injective ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ Eq (α := (n : ℕ) → ℝ≥0∞) (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have h : ∀ (n : ℕ),
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n
Tactic: funext n
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
n : ℕ
⊢ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n
have h : (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  HPow.hPow (β := ℕ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) 2
Tactic: rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ←
      coe_pow, sq, ← nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
n : ℕ
h :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) 2
⊢ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n
have h₁ : (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  HPow.hPow (β := ℝ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑2 : ℝ)
Tactic: rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ←
      coe_pow, sq, ← nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
n : ℕ
h :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) 2
h₁ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑2 : ℝ)
⊢ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n
have h₂ : (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  (↑‖a ^ n‖₊ : ℝ≥0∞) ^ (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑2 : ℝ))
Tactic: rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ←
      coe_pow, sq, ← nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
n : ℕ
h :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) 2
h₁ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑2 : ℝ)
h₂ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑‖a ^ n‖₊ : ℝ≥0∞) ^ (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑2 : ℝ))
⊢ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n
have h₃ : (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  (↑‖a ^ n‖₊ : ℝ≥0∞) ^ ((↑2 : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ←
      coe_pow, sq, ← nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
n : ℕ
h :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) 2
h₁ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) ((↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) (↑2 : ℝ)
h₂ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑‖a ^ n‖₊ : ℝ≥0∞) ^ (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) * (↑2 : ℝ))
h₃ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑‖a ^ n‖₊ : ℝ≥0∞) ^ ((↑2 : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    ((fun (x : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) n
have h₄ : (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  HPow.hPow (β := ℝ) (↑‖a ^ n‖₊ : ℝ≥0∞) (↑2 : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ←
      coe_pow, sq, ← nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]