awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
hk₁ : k⁻¹ ∈ spectrum.{u_1, u_2} 𝕜 (A := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)
⊢ k ≠ 0

Tactic:
rw [← inv_inv (Unitary.toUnits u), ← spectrum.map_inv, Set.mem_inv] at hk

Premises used: Unitary.toUnits, spectrum.map_inv, inv_inv, DFunLike.coe, Set.mem_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ ‖k‖⁻¹ ≤ norm.{u_2} (E := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)

Tactic:
simpa only [norm_inv] using norm_le_norm_of_mem hk

Premises used: spectrum.norm_le_norm_of_mem, norm_inv
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ ‖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
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
this : ‖k‖⁻¹ ≤ norm.{u_2} (E := E) (↑((toUnits : (a : ↥(unitary E)) → Eˣ) u)⁻¹ : E)
⊢ 1 ≤ ‖k‖

Tactic:
simpa using inv_le_of_inv_le₀ (norm_pos_iff.mpr hnk) this

Premises used: Iff.mpr, norm_pos_iff, inv_le_of_inv_le₀
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 : E
h : Membership.mem (γ := Submonoid E) (unitary E) u
⊢ σ 𝕜 u ⊆ Metric.sphere 0 1

Tactic:
Unitary.spectrum_subset_circle ⟨u, h⟩

Premises used: Subtype.mk, Unitary.spectrum_subset_circle
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 : E
hu : Membership.mem (γ := Submonoid E) (unitary E) u
z : 𝕜
hz : z ∈ σ 𝕜 u
⊢ ‖z‖ = 1

Tactic:
simpa using spectrum.subset_circle_of_unitary hu hz

Premises used: spectrum.subset_circle_of_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ quasispectrum ℝ≥0 a
⊢ x ∈ σ ℝ≥0 (A := Unitization ℂ A) (↑a : Unitization ℂ A)

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx

Premises used: NNReal, Unitization.quasispectrum_eq_spectrum_inr', Complex
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 (A := Unitization ℂ A) (↑a : Unitization ℂ A)
⊢ x ≤ ‖a‖₊

Tactic:
simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx

Premises used: spectrum.le_nnnorm_of_mem, Unitization.nnnorm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))

Tactic:
have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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∞)

Tactic:
tendsto_nhds_unique ?_ hconst

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
refine : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (spectralRadius ℂ a))
⊢ spectralRadius ℂ a = (↑‖a‖₊ : ℝ≥0∞)

Tactic:
refine tendsto_nhds_unique ?_ hconst

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) atTop
    (𝓝 (spectralRadius ℂ a))

Tactic:
(spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two)

Premises used: spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, tendsto_pow_atTop_atTop_of_one_lt, one_lt_two, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
h :
  Eq (α := ℕ → ℝ≥0∞) (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞))
    ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n)
⊢ Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (spectralRadius ℂ a))

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

Premises used: spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, tendsto_pow_atTop_atTop_of_one_lt, one_lt_two, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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)

Tactic:
funext fun n => ?_

Premises used: funext
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
h :
  ∀ (n : ℕ),
    (↑‖a‖₊ : ℝ≥0∞) =
      ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) n
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞))
    ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n)

Tactic:
refine funext fun n => ?_

Premises used: funext
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun (_n : ℕ) ↦ (↑‖a‖₊ : ℝ≥0∞)) atTop (𝓝 (↑‖a‖₊ : ℝ≥0∞))
n : ℕ
h :
  (↑‖a‖₊ : ℝ≥0∞) =
    (↑‖a‖₊ : ℝ≥0∞) ^ ((↑(HPow.hPow (α := ℕ) 2 n) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (α := ℕ) 2 n) : ℝ))
⊢ (↑‖a‖₊ : ℝ≥0∞) =
    ((fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (n : ℕ) ↦ HPow.hPow (α := ℕ) 2 n) n

Tactic:
rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_natCast, ENNReal.coe_pow, Function.comp_apply, IsSelfAdjoint.nnnorm_pow_two_pow
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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∞) =
    (↑‖a‖₊ : ℝ≥0∞) ^ ((↑(HPow.hPow (α := ℕ) 2 n) : ℝ) * HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (α := ℕ) 2 n) : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
⊢ spectralRadius ℂ a = (↑‖a‖₊ : ℝ≥0∞)

Tactic:
(ENNReal.pow_right_strictMono two_ne_zero).injective ?_

Premises used: ENNReal.pow_right_strictMono, two_ne_zero, StrictMono.injective
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
refine : HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2
⊢ spectralRadius ℂ a = (↑‖a‖₊ : ℝ≥0∞)

Tactic:
refine (ENNReal.pow_right_strictMono two_ne_zero).injective ?_

Premises used: ENNReal.pow_right_strictMono, two_ne_zero, StrictMono.injective
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
inst_1 : IsStarNormal a
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
⊢ 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:
funext n
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 : ℝ)
h₁₀ 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

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]

Premises used: star_comm_self', ENNReal.rpow_mul, ENNReal.rpow_natCast, sq, Commute.mul_pow, ENNReal.coe_pow, mul_comm, Function.comp_apply, CStarRing.nnnorm_star_mul_self, star_pow
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 : ℝ))

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]
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 : ℝ))
⊢ 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)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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))
⊢ Tendsto (fun (n : ℕ) ↦ (↑‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
    (𝓝 (HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2))

Tactic:
rw [← heq] at h₂
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 = spectralRadius ℂ (a⋆ * a)

Tactic:
tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))

Premises used: HMul.hMul, spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, tendsto_nhds_unique, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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 = spectralRadius ℂ (a⋆ * a)
⊢ HPow.hPow (β := ℕ) (spectralRadius ℂ a) 2 = HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2

Tactic:
convert! tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))

Premises used: HMul.hMul, spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, tendsto_nhds_unique, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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∞)
h₄ h₅ : (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞) = (↑‖a‖₊ : ℝ≥0∞) * (↑‖a‖₊ : ℝ≥0∞)
⊢ HPow.hPow (β := ℕ) (↑‖a‖₊ : ℝ≥0∞) 2 = spectralRadius ℂ (a⋆ * a)

Tactic:
rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]

Premises used: IsSelfAdjoint.star_mul_self, sq, ENNReal.coe_mul, IsSelfAdjoint.spectralRadius_eq_nnnorm, CStarRing.nnnorm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
rw : ‖a⋆ * a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₁ : ‖a‖ * ‖a‖ = HPow.hPow (β := ℕ) ‖a‖ 2
rw₂ rw₃ : HPow.hPow (β := ℕ) ‖a‖ 2 = HPow.hPow (β := ℕ) ‖a‖ 2
⊢ (spectralRadius ℂ (a⋆ * a)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
rw [(IsSelfAdjoint.star_mul_self a).toReal_spectralRadius_complex_eq_norm,
    CStarRing.norm_star_mul_self, ← pow_two]

Premises used: IsSelfAdjoint.star_mul_self, pow_two, IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm, CStarRing.norm_star_mul_self
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
rw₂ rw₃ : (spectralRadius ℂ (a * a⋆)).toReal = (spectralRadius ℂ (a * a⋆)).toReal
⊢ (spectralRadius ℂ (a * a⋆)).toReal = HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
rw [← norm_star a, ← toReal_spectralRadius_star_mul_self_eq_norm_sq, star_star]

Premises used: norm_star, star_star, CStarAlgebra.toReal_spectralRadius_star_mul_self_eq_norm_sq
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
⊢ √(spectralRadius ℂ (a⋆ * a)).toReal = ‖a‖

Tactic:
simp [toReal_spectralRadius_star_mul_self_eq_norm_sq]

Premises used: CStarAlgebra.toReal_spectralRadius_star_mul_self_eq_norm_sq
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
⊢ √(spectralRadius ℂ (a * a⋆)).toReal = ‖a‖

Tactic:
simp [toReal_spectralRadius_self_mul_star_eq_norm_sq]

Premises used: CStarAlgebra.toReal_spectralRadius_self_mul_star_eq_norm_sq
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
let : ∀ (this : NormedAlgebra ℚ A), z = (↑z.re : ℂ)
⊢ z = (↑z.re : ℂ)

Tactic:
let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this : NormedAlgebra ℚ A
⊢ 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)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ NormedSpace.exp (I • z) ∈ σ ℂ (NormedSpace.exp (I • a))

Tactic:
simpa only [Units.smul_def, Units.val_mk0] using
      spectrum.exp_mem_exp (Iu • a) (smul_mem_smul_iff.mpr hz)

Premises used: Iff.mpr, spectrum.smul_mem_smul_iff, Units.smul_def, spectrum.exp_mem_exp, HSMul.hSMul, Units.val_mk0
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
⊢ 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)
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this_1 : NormedAlgebra ℚ A
hu : Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (I • a))
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : NormedSpace.exp (I • z) ∈ σ ℂ (NormedSpace.exp (I • a))
⊢ z.im = (↑z.re : ℂ).im

Tactic:
simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff,
      smul_eq_mul, I_mul, neg_eq_zero] using
      spectrum.subset_circle_of_unitary hu this

Premises used: Complex.exp_eq_exp_ℂ, Real.exp_eq_one_iff, neg_eq_zero, mem_sphere_zero_iff_norm, Complex.I_mul, Complex.norm_exp, smul_eq_mul, spectrum.subset_circle_of_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
this_1 : NormedAlgebra ℚ A
hu : Membership.mem (γ := Submonoid A) (unitary A) (NormedSpace.exp (I • a))
Iu : ℂˣ := Units.mk0 I I_ne_zero
this : NormedSpace.exp (I • z) ∈ σ ℂ (NormedSpace.exp (I • a))
⊢ z = (↑z.re : ℂ)

Tactic:
exact Complex.ext (ofReal_re _) <| by
    simpa only [← Complex.exp_eq_exp_ℂ, mem_sphere_zero_iff_norm, norm_exp, Real.exp_eq_one_iff,
      smul_eq_mul, I_mul, neg_eq_zero] using
      spectrum.subset_circle_of_unitary hu this

Premises used: Complex.ext, Complex.ofReal_re
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : ↥(selfAdjoint A)
z : ℂ
hz : z ∈ σ ℂ (↑a : A)
⊢ z = (↑z.re : ℂ)

Tactic:
a.prop.mem_spectrum_eq_re hz

Premises used: Subtype.prop, IsSelfAdjoint.mem_spectrum_eq_re
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ z.im = 0

Tactic:
rw [ha.mem_spectrum_eq_re hz, ofReal_im]

Premises used: IsSelfAdjoint.mem_spectrum_eq_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : A
ha : IsSelfAdjoint a
z : ℂ
hz : z ∈ σ ℂ a
⊢ (ofReal ∘ re) z ∈ σ ℂ a

Tactic:
simpa only [(ha.mem_spectrum_eq_re hz).symm, Function.comp_apply] using hz

Premises used: IsSelfAdjoint.mem_spectrum_eq_re, Function.comp_apply, Eq.symm
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : StarModule ℂ A
a : ↥(selfAdjoint A)
⊢ σ ℂ (↑a : A) = ofReal ∘ re '' σ ℂ (↑a : A)

Tactic:
a.property.val_re_map_spectrum

Premises used: IsSelfAdjoint.val_re_map_spectrum, Subtype.property
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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)ᶜ ∩ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0})

Tactic:
rw [← Set.inter_union_distrib_left, ← Set.setOf_or] at this

Premises used: Set.setOf_or, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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})
rw : IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)
⊢ IsConnected (σ ℂ a)ᶜ

Tactic:
rw [← Set.inter_univ (σ ℂ a)ᶜ]

Premises used: spectrum, Compl.compl, Set.inter_univ, Complex
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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)ᶜ ∩ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0})

Tactic:
this
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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})
h : Eq (α := Set ℂ) Set.univ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0}
⊢ IsConnected ((σ ℂ a)ᶜ ∩ Set.univ)

Tactic:
convert! this using 2
-- Module: Mathlib.Analysis.CStarAlgebra.Spectrum
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})
⊢ Eq (α := Set ℂ) Set.univ {a : ℂ | 0 ≤ a.im ∨ a.im ≤ 0}

Tactic:
Eq.symm <| Set.eq_univ_of_forall (fun z ↦ le_total 0 z.im)

Premises used: Complex.im, le_total, Set.eq_univ_of_forall, OfNat.ofNat, Eq.symm