awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ k ≠ 0

Tactic:
have hk : k ≠ 0 :=
    ne_zero_of_norm_ne_zero ((mul_nonneg (norm_nonneg _) (norm_nonneg _)).trans_lt h).ne'
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
⊢ ‖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

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, inv_pos, inv_inv, mul_inv_lt_iff₀', one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
h₁ : ‖a‖ < (norm.{u_2} (E := A) 1)⁻¹ * ‖k‖
⊢ Nontrivial A

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

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, inv_pos, inv_inv, mul_inv_lt_iff₀', one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
h₁ : ‖a‖ < (norm.{u_2} (E := A) 1)⁻¹ * ‖k‖
a₁ : Nontrivial A
⊢ k ≠ 0

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

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, inv_pos, inv_inv, mul_inv_lt_iff₀', one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
⊢ ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹

Tactic:
simpa [ku, norm_algebraMap] using h

Premises used: norm_algebraMap
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
⊢ ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹

Tactic:
have hku : ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹ := by simpa [ku, norm_algebraMap] using h
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
hku : ‖-a‖ < ‖(↑ku⁻¹ : A)‖⁻¹
⊢ IsUnit (HSMul.hSMul (β := A) k 1 - a)

Tactic:
simpa [ku, sub_eq_add_neg, Algebra.algebraMap_eq_smul_one] using (ku.add (-a) hku).isUnit

Premises used: sub_eq_add_neg, Algebra.algebraMap_eq_smul_one, Units.add, Units.isUnit, Neg.neg
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖
rwa : ‖a‖ * 1 < ‖k‖
rwa₁ rwa₂ rwa₃ rwa₄ : ‖a‖ < ‖k‖
⊢ ‖a‖ * norm.{u_2} (E := A) 1 < ‖k‖

Tactic:
rwa [norm_one, mul_one]

Premises used: NormOneClass.norm_one, mul_one
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
⊢ ‖k‖ ≤ ‖a‖ * norm.{u_2} (E := A) 1

Tactic:
le_of_not_gt <| mt mem_resolventSet_of_norm_lt_mul hk

Premises used: le_of_not_gt, mt, spectrum.mem_resolventSet_of_norm_lt_mul
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
⊢ ‖k‖ ≤ ‖a‖

Tactic:
le_of_not_gt <| mt mem_resolventSet_of_norm_lt hk

Premises used: le_of_not_gt, mt, spectrum.mem_resolventSet_of_norm_lt
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 (‖a‖ * norm.{u_2} (E := A) 1)) k

Tactic:
simp [norm_le_norm_mul_of_mem hk]

Premises used: spectrum.norm_le_norm_mul_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 ‖a‖) k

Tactic:
simp [norm_le_norm_of_mem hk]

Premises used: spectrum.norm_le_norm_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
⊢ Bornology.IsBounded (σ a)

Tactic:
Metric.isBounded_closedBall.subset (subset_closedBall_norm_mul a)

Premises used: Metric.isBounded_closedBall, spectrum.subset_closedBall_norm_mul, Bornology.IsBounded.subset
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ IsCompact (σ a)

Tactic:
Metric.isCompact_of_isClosed_isBounded (spectrum.isClosed a) (isBounded a)

Premises used: Metric.isCompact_of_isClosed_isBounded, spectrum.isClosed, spectrum.isBounded
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ CompactSpace.{u_1} (↑(σ a) : Type u_1)

Tactic:
isCompact_iff_compactSpace.mp <| spectrum.isCompact a

Premises used: isCompact_iff_compactSpace, spectrum.isCompact, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
rw : IsCompact (spectrum ℝ a) → IsCompact (spectrum ℝ≥0 a)
⊢ CompactSpace (↑(spectrum ℝ≥0 a) : Type)

Tactic:
rw [← isCompact_iff_compactSpace] at *

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
rw : IsCompact (X := ℝ≥0) ((⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) ⁻¹' spectrum ℝ a)
⊢ IsCompact (spectrum ℝ≥0 a)

Tactic:
rw [← preimage_algebraMap ℝ]

Premises used: Real, spectrum.preimage_algebraMap
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 ℝ a)

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 (X := ℝ≥0) ((⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) ⁻¹' spectrum ℝ a)

Tactic:
exact isClosed_nonneg.isClosedEmbedding_subtypeVal.isCompact_preimage <| by assumption

Premises used: isClosed_nonneg, Topology.IsClosedEmbedding.isCompact_preimage, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_3
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : A
inst_2 : CompactSpace (↑(spectrum ℝ a) : Type)
rw : CompactSpace (↑(spectrum ℝ≥0 a) : Type)
⊢ IsCompact (spectrum ℝ≥0 a)

Tactic:
rw [isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_3
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : A
inst_2 : CompactSpace (↑(spectrum ℝ a) : Type)
⊢ CompactSpace (↑(spectrum ℝ≥0 a) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
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)))
⊢ IsCompact (quasispectrum 𝕜 a)

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜,
    ← AlgEquiv.spectrum_eq (WithLp.unitizationAlgEquiv 𝕜).symm (a : Unitization 𝕜 B)]

Premises used: WithLp.unitizationAlgEquiv, AlgEquiv.symm, Unitization.inr, AlgEquiv.spectrum_eq, Unitization.quasispectrum_eq_spectrum_inr'
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
    (σ (A := WithLp 1 (Unitization 𝕜 B))
      ((AlgEquiv.symm (WithLp.unitizationAlgEquiv 𝕜) : (a : Unitization 𝕜 B) → WithLp 1 (Unitization 𝕜 B))
          (↑a : Unitization 𝕜 B) :
        WithLp 1 (Unitization 𝕜 B)))

Tactic:
spectrum.isCompact _

Premises used: spectrum.isCompact
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
    (σ (A := WithLp 1 (Unitization 𝕜 B))
      ((AlgEquiv.symm (WithLp.unitizationAlgEquiv 𝕜) : (a : Unitization 𝕜 B) → WithLp 1 (Unitization 𝕜 B))
          (↑a : Unitization 𝕜 B) :
        WithLp 1 (Unitization 𝕜 B)))

Tactic:
exact spectrum.isCompact _

Premises used: spectrum.isCompact
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 𝕜
a : B
⊢ CompactSpace.{u_1} (↑(quasispectrum 𝕜 a) : Type u_1)

Tactic:
isCompact_iff_compactSpace.mp <| quasispectrum.isCompact a

Premises used: isCompact_iff_compactSpace, quasispectrum.isCompact, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
rw : IsCompact (quasispectrum ℝ a) → IsCompact (quasispectrum ℝ≥0 a)
⊢ CompactSpace (↑(quasispectrum ℝ≥0 a) : Type)

Tactic:
rw [← isCompact_iff_compactSpace] at *

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
rw : IsCompact (X := ℝ≥0) ((⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) ⁻¹' quasispectrum ℝ a)
⊢ IsCompact (quasispectrum ℝ≥0 a)

Tactic:
rw [← quasispectrum.preimage_algebraMap ℝ]

Premises used: Real, quasispectrum.preimage_algebraMap
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 ℝ a)

Tactic:
assumption
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 (X := ℝ≥0) ((⇑(algebraMap ℝ≥0 ℝ) : (a : ℝ≥0) → ℝ) ⁻¹' quasispectrum ℝ a)

Tactic:
exact isClosed_nonneg.isClosedEmbedding_subtypeVal.isCompact_preimage <| by assumption

Premises used: isClosed_nonneg, Topology.IsClosedEmbedding.isCompact_preimage, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
rw : CompactSpace (↑(quasispectrum ℝ≥0 a) : Type)
⊢ IsCompact (quasispectrum ℝ≥0 a)

Tactic:
rw [isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
⊢ CompactSpace (↑(quasispectrum ℝ≥0 a) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_3
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
inst_3 : NormOneClass A
a : A
r : ℝ≥0
hr : r ∈ spectrum ℝ≥0 a
⊢ r ≤ ‖a‖₊

Tactic:
calc
  r ≤ ‖(r : ℝ)‖ := Real.le_norm_self _
  _ ≤ ‖a‖       := norm_le_norm_of_mem hr

Premises used: spectrum.norm_le_norm_of_mem, Trans.trans, Real.le_norm_self, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_3
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
inst_3 : NormOneClass A
a : A
r : ℝ≥0
hr : r ∈ spectrum ℝ≥0 a
⊢ (↑r : ℝ) ≤ ‖a‖

Tactic:
coe_mono <| le_nnnorm_of_mem hr

Premises used: NNReal.coe_mono, spectrum.le_nnnorm_of_mem, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)

Tactic:
iSup₂_le fun k hk => ?_

Premises used: iSup₂_le, spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
refine : ∀ (k : 𝕜) (hk : k ∈ σ a), (↑‖k‖₊ : ℝ≥0∞) ≤ (↑‖a‖₊ : ℝ≥0∞)
⊢ spectralRadius 𝕜 a ≤ (↑‖a‖₊ : ℝ≥0∞)

Tactic:
refine iSup₂_le fun k hk => ?_

Premises used: iSup₂_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤ (↑‖a‖₊ : ℝ≥0∞)

Tactic:
mod_cast norm_le_norm_of_mem hk

Premises used: spectrum.norm_le_norm_of_mem, cast, ENNReal.coe_le_coe._simp_1, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
⊢ (↑‖k‖₊ : ℝ≥0∞) ≤ (↑‖a‖₊ : ℝ≥0∞)

Tactic:
exact mod_cast norm_le_norm_of_mem hk

Premises used: spectrum.norm_le_norm_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
obtain :
  ∀ (k : 𝕜) (hk : k ∈ σ a) (h : IsMaxOn (β := ℝ≥0) (fun (a : 𝕜) ↦ ‖a‖₊) (σ a) k),
    ∃ k ∈ σ a, (↑‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a
⊢ ∃ k ∈ σ a, (↑‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a

Tactic:
obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn

Premises used: Continuous.continuousOn, spectrum.isCompact, continuous_nnnorm, IsCompact.exists_isMaxOn
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
h : IsMaxOn (β := ℝ≥0) (fun (a : 𝕜) ↦ ‖a‖₊) (σ a) k
⊢ ∃ k ∈ σ a, (↑‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a

Tactic:
⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩

Premises used: iSup₂_le, spectrum, le_iSup₂, cast, Membership.mem, le_antisymm, ENNReal.coe_le_coe._simp_1, implies_congr, And.intro, Exists.intro, Eq.refl, Eq.symm, forall_congr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : 𝕜
hk : k ∈ σ a
h : IsMaxOn (β := ℝ≥0) (fun (a : 𝕜) ↦ ‖a‖₊) (σ a) k
⊢ ∃ k ∈ σ a, (↑‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a

Tactic:
exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
r : ℝ≥0
hr : ∀ k ∈ σ a, ‖k‖₊ < r
⊢ ∀ x ∈ σ a, ‖x‖ₑ < (↑r : ℝ≥0∞)

Tactic:
simpa using hr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)

Tactic:
iSup₂_le fun k hk => ?_

Premises used: iSup₂_le, spectralRadius
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℕ
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)
⊢ spectralRadius 𝕜 a ≤
    (↑‖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 => ?_

Premises used: iSup₂_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 ^ (n + 1) ∈ σ (a ^ (n + 1))

Tactic:
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⟩

Premises used: Polynomial.monomial, one_smul, Algebra.algebraMap_eq_smul_one, spectrum.subset_polynomial_aeval, HAdd.hAdd, And.intro, Exists.intro, Polynomial.aeval_monomial, OfNat.ofNat, DFunLike.coe, one_mul, rfl, Polynomial.eval_monomial
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 ^ (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⟩
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊ ^ (n + 1)) : ℝ≥0∞) ≤ (↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)

Tactic:
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))

Premises used: Real.toNNReal_mul, spectrum.norm_le_norm_mul_of_mem, nnnorm_pow, Real.toNNReal_mono, ENNReal.coe_mul, HAdd.hAdd, ENNReal.coe_mono, OfNat.ofNat, norm_toNNReal, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊ ^ (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))
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)
⊢ LT.lt (α := ℝ) 0 (↑(n + 1) : ℝ)

Tactic:
have hn : 0 < ((n + 1 : ℕ) : ℝ) := mod_cast Nat.succ_pos'
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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) : ℝ)
⊢ LE.le (α := ℝ≥0∞) ((fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)) (↑(‖k‖₊ ^ (n + 1)) : ℝ≥0∞))
    ((fun (x : ℝ≥0∞) ↦ x ^ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
      ((↑‖a ^ (n + 1)‖₊ : ℝ≥0∞) * (↑(nnnorm.{u_2} (E := A) 1) : ℝ≥0∞)))

Tactic:
monotone_rpow_of_nonneg (one_div_pos.mpr hn).le nnnorm_pow_le

Premises used: Iff.mpr, ENNReal.monotone_rpow_of_nonneg, LT.lt.le, one_div_pos