awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ))
h₄ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) (↑‖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]
-- 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 : ℝ))
h₄ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) (↑‖a ^ n‖₊ : ℝ≥0∞) (↑2 : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₅ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) (↑‖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‖₊ 2) : ℝ≥0∞) ^ 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 : ℝ))
h₄ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) (↑‖a ^ n‖₊ : ℝ≥0∞) (↑2 : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₅ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) (↑‖a ^ n‖₊ : ℝ≥0∞) 2 ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₆ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(HPow.hPow (β := ℕ) ‖a ^ n‖₊ 2) : ℝ≥0∞) ^ 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 : ℝ) =
  (↑(‖a ^ n‖₊ * ‖a ^ n‖₊) : ℝ≥0∞) ^ 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 : ℝ))
h₄ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) (↑‖a ^ n‖₊ : ℝ≥0∞) (↑2 : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₅ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) (↑‖a ^ n‖₊ : ℝ≥0∞) 2 ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₆ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(HPow.hPow (β := ℕ) ‖a ^ n‖₊ 2) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₇ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(‖a ^ n‖₊ * ‖a ^ n‖₊) : ℝ≥0∞) ^ 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 : ℝ) =
  (↑‖(a ^ n)⋆ * a ^ n‖₊ : ℝ≥0∞) ^ 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 : ℝ))
h₄ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) (↑‖a ^ n‖₊ : ℝ≥0∞) (↑2 : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₅ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) (↑‖a ^ n‖₊ : ℝ≥0∞) 2 ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₆ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(HPow.hPow (β := ℕ) ‖a ^ n‖₊ 2) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₇ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(‖a ^ n‖₊ * ‖a ^ n‖₊) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₈ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑‖(a ^ n)⋆ * a ^ n‖₊ : ℝ≥0∞) ^ 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⋆ ^ n * a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  (↑‖(a ^ n)⋆ * a ^ n‖₊ : ℝ≥0∞) ^ 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 : ℝ))
h₄ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℝ) (↑‖a ^ n‖₊ : ℝ≥0∞) (↑2 : ℝ) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₅ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    HPow.hPow (β := ℕ) (↑‖a ^ n‖₊ : ℝ≥0∞) 2 ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₆ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(HPow.hPow (β := ℕ) ‖a ^ n‖₊ 2) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₇ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑(‖a ^ n‖₊ * ‖a ^ n‖₊) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₈ :
  (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑‖(a ^ n)⋆ * a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
h₉ :
  (↑‖a⋆ ^ n * a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
    (↑‖(a ^ n)⋆ * a ^ n‖₊ : ℝ≥0∞) ^ 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⋆ ^ n * a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) =
  (↑‖a⋆ ^ n * a ^ n‖₊ : ℝ≥0∞) ^ 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 (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2
have heq : 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 : ℝ))
Tactic: have heq :
    (fun n : ℕ => (‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) =
      (fun x => x ^ 2) ∘ fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) := by
    funext n
    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 (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
heq :
  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 : ℝ))
⊢ HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2
have h₂ : Tendsto (α := ℕ)
  ((fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) a 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
  (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
Tactic: have h₂ :=
    ((ENNReal.continuous_pow 2).tendsto (spectralRadius ℂ a)).comp
      (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
heq :
  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 : ℝ))
h₂ :
  Tendsto (α := ℕ)
    ((fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℕ) a 2) ∘ fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
⊢ HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2
have h₃ : Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
  (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
Tactic: rw [← heq] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
heq :
  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 : ℝ))
h₂ :
  Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
⊢ HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2
have h : HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = spectralRadius ℂ (a⋆ * a)
Tactic: convert! tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
heq :
  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 : ℝ))
h₂ :
  Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
⊢ HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = spectralRadius ℂ (a⋆ * a)
have h : HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
Tactic: rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_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
heq :
  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 : ℝ))
h₂ :
  Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
h : HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
⊢ HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = spectralRadius ℂ (a⋆ * a)
have h₁ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
Tactic: rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_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
heq :
  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 : ℝ))
h₂ :
  Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
h : HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
h₁ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
⊢ HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = spectralRadius ℂ (a⋆ * a)
have h₃ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑(‖a‖₊ * ‖a‖₊) : ℝ≥0∞)
Tactic: rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_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
heq :
  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 : ℝ))
h₂ :
  Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))
h : HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
h₁ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑‖a⋆ * a‖₊ : ℝ≥0∞)
h₃ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑(‖a‖₊ * ‖a‖₊) : ℝ≥0∞)
⊢ HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = spectralRadius ℂ (a⋆ * a)
have h₄ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞)
Tactic: rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a⋆ * a)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2
have rw : ‖a⋆ * a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
Tactic: rw [(IsSelfAdjoint.star_mul_self a).toReal_spectralRadius_complex_eq_norm,
    CStarRing.norm_star_mul_self, ← pow_two]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
rw : ‖a⋆ * a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
⊢ (spectralRadius ℂ (a⋆ * a)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2
have rw₁ : ‖a‖ * ‖a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
Tactic: rw [(IsSelfAdjoint.star_mul_self a).toReal_spectralRadius_complex_eq_norm,
    CStarRing.norm_star_mul_self, ← pow_two]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
rw : ‖a⋆ * a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖a‖ * ‖a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
⊢ (spectralRadius ℂ (a⋆ * a)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2
have rw₂ : HPow.hPow (β := ℕ) ‖a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
Tactic: rw [(IsSelfAdjoint.star_mul_self a).toReal_spectralRadius_complex_eq_norm,
    CStarRing.norm_star_mul_self, ← pow_two]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
⊢ (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2
have rw : (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a⋆‖ 2
Tactic: rw [← norm_star a, ← toReal_spectralRadius_star_mul_self_eq_norm_sq, star_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
rw : (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a⋆‖ 2
⊢ (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2
have rw₁ : (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a⋆⋆ * a⋆)).toReal
Tactic: rw [← norm_star a, ← toReal_spectralRadius_star_mul_self_eq_norm_sq, star_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
rw : (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a⋆‖ 2
rw₁ : (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a⋆⋆ * a⋆)).toReal
⊢ (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2
have rw₂ : (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a * a⋆)).toReal
Tactic: rw [← norm_star a, ← toReal_spectralRadius_star_mul_self_eq_norm_sq, star_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ z = (↑z.re : ℂ)
have let : ∀ (this : NormedAlgebra ℚ A), z = (↑z.re : ℂ)
Tactic: let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this : NormedAlgebra ℚ A
⊢ z = (↑z.re : ℂ)
have hu : Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (I • a))
Tactic: have hu := exp_mem_unitary_of_mem_skewAdjoint (ha.smul_mem_skewAdjoint conj_I)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this : NormedAlgebra ℚ A
hu : Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (I • a))
Iu : ℂˣ := Units.mk0 I I_ne_zero
⊢ z = (↑z.re : ℂ)
have this₁ : NormedSpace.exp (I • z) ∈ σ ℂ (NormedSpace.exp (I • a))
Tactic: have : NormedSpace.exp (I • z) ∈ spectrum ℂ (NormedSpace.exp (I • a)) := by
    simpa only [Units.smul_def, Units.val_mk0] using
      spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ z.im = 0
have rw : (↑z.re : ℂ).im = 0
Tactic: rw [ha.mem_spectrum_eq_re hz, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
rw : (↑z.re : ℂ).im = 0
⊢ z.im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [ha.mem_spectrum_eq_re hz, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ
have this₁ : IsConnected ((σ ℂ a)ᶜ ∩ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0})
Tactic: rw [← Set.inter_union_distrib_left, ← Set.setOf_or] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected (σ ℂ a)ᶜ
have rw : IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)
Tactic: rw [← Set.inter_univ (σ ℂ a)ᶜ]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
this : IsConnected ((σ ℂ a)ᶜ ∩ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0})
⊢ IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)
have h : Eq (α := Set ℂ) Set.univ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0}
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected (σ ℂ a)ᶜ
have suffices : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
Tactic: suffices IsConnected (((σ ℂ a)ᶜ ∩ {z | 0 ≤ z.im}) ∪ (σ ℂ a)ᶜ ∩ {z | z.im ≤ 0}) by
    rw [← Set.inter_union_distrib_left, ← Set.setOf_or] at this
    rw [← Set.inter_univ (σ ℂ a)ᶜ]
    convert! this using 2
    exact Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
have refine : ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})).Nonempty
Tactic: refine IsConnected.union ?nonempty ?upper ?lower
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
refine : ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})).Nonempty
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
have upper : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})
Tactic: refine IsConnected.union ?nonempty ?upper ?lower
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.Spectrum (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
refine : ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∩ ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})).Nonempty
upper : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im})
⊢ IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | 0 ≤ z.im} ∪ (σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
have lower : IsConnected ((σ ℂ a)ᶜ ∩ {z : ℂ | z.im ≤ 0})
Tactic: refine IsConnected.union ?nonempty ?upper ?lower