awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
⊢ k ∈ ρ a
have rw : IsUnit (HSMul.hSMul (β := A) k 1 - a)
Tactic: rw [resolventSet, Set.mem_setOf_eq, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
⊢ IsUnit (HSMul.hSMul (β := A) k 1 - a)
have a₁ : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
h_1 : Nontrivial A
⊢ IsUnit (HSMul.hSMul (β := A) k 1 - a)
have hk : k ≠ 0
Tactic: have hk : k ≠ 0 :=
    ne_zero_of_norm_ne_zero ((mul_nonneg (norm_nonneg _) (norm_nonneg _)).trans_lt h).ne'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
h_1 : Nontrivial A
hk : k ≠ 0
ku : Aˣ := ((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u_1, u_2} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ) (Units.mk0 k hk)
⊢ IsUnit (HSMul.hSMul (β := A) k 1 - a)
have h₁ : ‖a‖ < (norm.{u_2} (E := A) 1)⁻¹ * ‖k‖
Tactic: rw [← inv_inv ‖(1 : A)‖,
    mul_inv_lt_iff₀' (inv_pos.2 <| norm_pos_iff.2 (one_ne_zero : (1 : A) ≠ 0))] at h
Cleared hypotheses: h, h_1, hk, ku
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
k : 𝕜
h : ‖a‖ < (norm.{u_2} (E := A) 1)⁻¹ * ‖k‖
h_1 : Nontrivial A
hk : k ≠ 0
ku : Aˣ := ((Units.map (↑↑ₐ : 𝕜 →* A) : MonoidHom.{u_1, u_2} 𝕜ˣ Aˣ) : (a : 𝕜ˣ) → Aˣ) (Units.mk0 k hk)
⊢ IsUnit (HSMul.hSMul (β := A) k 1 - a)
have hku : ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹
Tactic: have hku : ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹ := by simpa [ku, norm_algebraMap] using h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : NormOneClass A
a : A
k : 𝕜
h : ‖a‖ < ‖k‖
⊢ ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖
have rwa : ‖a‖ * 1 < ‖k‖
Tactic: rwa [norm_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A_1 : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A_1
inst_2 : NormedAlgebra 𝕜 A_1
inst_3 : CompleteSpace A_1
A : Type u_3
inst_4 : NormedRing A
inst_5 : NormedAlgebra ℝ A
a : A
inst_6 : CompactSpace (↑(spectrum ℝ a) : Type)
⊢ CompactSpace (↑(spectrum ℝ≥0 a) : Type)
have rw : IsCompact (spectrum ℝ a) → IsCompact (spectrum ℝ≥0 a)
Tactic: rw [← isCompact_iff_compactSpace] at *
Cleared hypotheses: inst_6
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A_1 : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A_1
inst_2 : NormedAlgebra 𝕜 A_1
inst_3 : CompleteSpace A_1
A : Type u_3
inst_4 : NormedRing A
inst_5 : NormedAlgebra ℝ A
a : A
inst_6 : IsCompact (spectrum ℝ a)
⊢ IsCompact (spectrum ℝ≥0 a)
have rw : IsCompact (X := ℝ≥0) ((⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) ⁻¹' spectrum ℝ a)
Tactic: rw [← preimage_algebraMap ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : A
inst_2 : CompactSpace (↑(spectrum ℝ a) : Type)
⊢ IsCompact (spectrum ℝ≥0 a)
have rw : CompactSpace (↑(spectrum ℝ≥0 a) : Type)
Tactic: rw [isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
B : Type u_3
inst_1 : NonUnitalNormedRing B
inst_2 : NormedSpace 𝕜 B
inst_3 : CompleteSpace B
inst_4 : IsScalarTower 𝕜 B B
inst_5 : SMulCommClass 𝕜 B B
inst_6 : ProperSpace 𝕜
a : B
⊢ IsCompact (quasispectrum 𝕜 a)
have rw : IsCompact
  (σ (A := WithLp 1 (Unitization 𝕜 B))
    ((AlgEquiv.symm (WithLp.unitizationAlgEquiv 𝕜) : (a : Unitization 𝕜 B) → WithLp 1 (Unitization 𝕜 B))
        (↑a : Unitization 𝕜 B) :
      WithLp 1 (Unitization 𝕜 B)))
Tactic: rw [Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜,
    ← AlgEquiv.spectrum_eq (WithLp.unitizationAlgEquiv 𝕜).symm (a : Unitization 𝕜 B)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
B : Type u_3
inst_4 : NonUnitalNormedRing B
inst_5 : NormedSpace 𝕜 B
inst_6 : CompleteSpace B
inst_7 : IsScalarTower 𝕜 B B
inst_8 : SMulCommClass 𝕜 B B
inst_9 : ProperSpace 𝕜
inst_10 : NormedSpace ℝ B
inst_11 : IsScalarTower ℝ B B
inst_12 : SMulCommClass ℝ B B
a : B
inst_13 : CompactSpace (↑(quasispectrum ℝ a) : Type)
⊢ CompactSpace (↑(quasispectrum ℝ≥0 a) : Type)
have rw : IsCompact (quasispectrum ℝ a) → IsCompact (quasispectrum ℝ≥0 a)
Tactic: rw [← isCompact_iff_compactSpace] at *
Cleared hypotheses: inst_13
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
B : Type u_3
inst_4 : NonUnitalNormedRing B
inst_5 : NormedSpace 𝕜 B
inst_6 : CompleteSpace B
inst_7 : IsScalarTower 𝕜 B B
inst_8 : SMulCommClass 𝕜 B B
inst_9 : ProperSpace 𝕜
inst_10 : NormedSpace ℝ B
inst_11 : IsScalarTower ℝ B B
inst_12 : SMulCommClass ℝ B B
a : B
inst_13 : IsCompact (quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)
have rw : IsCompact (X := ℝ≥0) ((⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) ⁻¹' quasispectrum ℝ a)
Tactic: rw [← quasispectrum.preimage_algebraMap ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
B : Type u_3
inst : NonUnitalNormedRing B
inst_1 : NormedSpace ℝ B
inst_2 : IsScalarTower ℝ B B
inst_3 : SMulCommClass ℝ B B
a : B
inst_4 : CompactSpace (↑(quasispectrum ℝ a) : Type)
⊢ IsCompact (quasispectrum ℝ≥0 a)
have rw : CompactSpace (↑(quasispectrum ℝ≥0 a) : Type)
Tactic: rw [isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : NormOneClass A
a : A
⊢ spectralRadius 𝕜 a ≤ (↑‖a‖₊ : ℝ≥0∞)
have refine : ∀ (k : 𝕜) (hk : k ∈ σ a), (↑‖k‖₊ : ℝ≥0∞) ≤ (↑‖a‖₊ : ℝ≥0∞)
Tactic: refine iSup₂_le fun k hk => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
a : A
ha : (σ a).Nonempty
⊢ ∃ k ∈ σ a, (↑‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a
have obtain : ∀ (k : 𝕜) (hk : k ∈ σ a) (h : IsMaxOn (β := ℝ≥0) (fun (a : 𝕜) ↦ ‖a‖₊) (σ a) k),
  ∃ k ∈ σ a, (↑‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a
Tactic: obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
⊢ spectralRadius 𝕜 a ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have refine : ∀ (k : 𝕜) (hk : k ∈ σ a),
  (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: refine iSup₂_le fun k hk => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
Tactic: have pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1)) := by
    simpa only [one_mul, Algebra.algebraMap_eq_smul_one, one_smul, aeval_monomial, one_mul,
      eval_monomial] using subset_polynomial_aeval a (@monomial 𝕜 _ (n + 1) (1 : 𝕜)) ⟨k, hk, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
Tactic: have nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ ‖a ^ (n + 1)‖₊ * ‖(1 : A)‖₊ := by
    simpa only [Real.toNNReal_mul (norm_nonneg _), norm_toNNReal, nnnorm_pow k (n + 1),
      ENNReal.coe_mul] using coe_mono (Real.toNNReal_mono (norm_le_norm_mul_of_mem pow_mem))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
Tactic: have hn : 0 < ((n + 1 : ℕ) : ℝ) := mod_cast Nat.succ_pos'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have h : (↑‖k‖₊ : ℝ≥0∞) = (fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞)
Tactic: convert! monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
h : (↑‖k‖₊ : ℝ≥0∞) = (fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞)
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤
    (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have h₁ : (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
    (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
  (fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
    ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞))
Tactic: convert! monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
⊢ (↑‖k‖₊ : ℝ≥0∞) = ((↑‖k‖₊ : ℝ≥0∞) ^ (n + 1)) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
have h : n + 1 ≠ 0
Tactic: rw [one_div, pow_rpow_inv_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
⊢ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
have h : (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
    (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
  ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [Nat.cast_succ, ENNReal.coe_mul_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
n : ℕ
k : 𝕜
hk : k ∈ σ a
pow_mem : k ^ (n + 1) ∈ σ (a ^ (n + 1))
nnnorm_pow_le : (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)
hn : LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)
h :
  (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
have h₁ : (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
    (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
  (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) *
    (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [Nat.cast_succ, ENNReal.coe_mul_rpow]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
have refine : ∀ (ε : ℝ≥0∞) (hε : ε < 1),
  ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
Tactic: refine ENNReal.le_of_forall_lt_one_mul_le fun ε hε => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
have pos : ∀ (h : ε = 0), ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
Tactic: by_cases h : ε = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
pos :
  ∀ (h : ε = 0),
    ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
have neg : ∀ (h : ¬ε = 0), ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
Tactic: by_cases h : ε = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ ε * spectralRadius 𝕜 a ≤ liminf (fun (n : ℕ) ↦ (↑‖a ^ n‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) atTop
have neg : spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
Tactic: simp only [ENNReal.mul_le_iff_le_inv h (hε.trans_le le_top).ne, mul_comm ε⁻¹,
    liminf_eq_iSup_iInf_of_nat', ENNReal.iSup_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
| ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
have arg : fun (i : ℕ) ↦ (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
i : ℕ
| (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
have h₁ : ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
Tactic: rw [ENNReal.iInf_mul (by simp [h])]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
| ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
have h₁ : ∀ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
Tactic: arg 1; intro i; rw [ENNReal.iInf_mul (by simp [h])]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤
    ⨆ (i : ℕ), (⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ)) * ε⁻¹
have neg : spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
Tactic: conv_rhs => arg 1; intro i; rw [ENNReal.iInf_mul (by simp [h])]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : ε < 1
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
have hε₁ : 1 < ε⁻¹
Tactic: rw [← ENNReal.inv_lt_inv, inv_one] at hε
Cleared hypotheses: hε, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
⊢ spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
have neg : ∀ (N : ℕ) (hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹),
  spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
Tactic: obtain ⟨N, hN⟩ := eventually_atTop.mp
    (ENNReal.eventually_pow_one_div_le (ENNReal.coe_ne_top : ↑‖(1 : A)‖₊ ≠ ∞) hε)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨆ (i : ℕ), ⨅ (i_1 : ℕ), (↑‖a ^ (i_1 + i)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i_1 + i) : ℝ) * ε⁻¹
have neg : spectralRadius 𝕜 a ≤ ⨅ (i : ℕ), (↑‖a ^ (i + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i + (N + 1)) : ℝ) * ε⁻¹
Tactic: refine le_trans ?_ (le_iSup _ (N + 1))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
⊢ spectralRadius 𝕜 a ≤ ⨅ (i : ℕ), (↑‖a ^ (i + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(i + (N + 1)) : ℝ) * ε⁻¹
have neg : ∀ (n : ℕ), spectralRadius 𝕜 a ≤ (↑‖a ^ (n + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + (N + 1)) : ℝ) * ε⁻¹
Tactic: refine le_iInf fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
⊢ spectralRadius 𝕜 a ≤ (↑‖a ^ (n + (N + 1))‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + (N + 1)) : ℝ) * ε⁻¹
have neg : spectralRadius 𝕜 a ≤ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
Tactic: simp only [← add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
⊢ spectralRadius 𝕜 a ≤ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
have neg : (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) *
    (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) ≤
  (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
Tactic: refine (spectralRadius_le_pow_nnnorm_pow_one_div 𝕜 a (n + N)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
ε : ℝ≥0∞
hε : 1 < ε⁻¹
h : ¬ε = 0
N : ℕ
hN : ∀ b ≥ N, (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ) ≤ ε⁻¹
n : ℕ
⊢ (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) *
      (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ (1 / HAdd.hAdd (α := ℝ) (↑(n + N) : ℝ) 1) ≤
    (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
have neg : (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) *
    (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) ≤
  (↑‖a ^ (n + N + 1)‖₊ : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑(n + N + 1) : ℝ) * ε⁻¹
Tactic: norm_cast