awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
⊢ frontier (σ 𝕜 (↑x : A)) ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x) ∪
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))
have apply : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
  frontier (σ 𝕜 (↑x : A))
Tactic: apply union_subset <| inter_subset_left
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
this : CompleteSpace.{u_4} ↥S
h_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 x \ σ 𝕜 (↑x : A))
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (σ 𝕜 (↑x : A))ᶜ ∩ frontier (σ 𝕜 x) ⊆
    frontier (σ 𝕜 (↑x : A))
have refine : frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (↑x : A))
Tactic: refine inter_subset_inter_right _ ?_ |>.trans <| inter_subset_right
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
have pos : ∀ (hz' : z ∈ σ 𝕜 (↑x : A)), Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
Tactic: by_cases hz' : z ∈ σ 𝕜 (x : A)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
pos : ∀ (hz' : z ∈ σ 𝕜 (↑x : A)), Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
have neg : ∀ (hz' : z ∉ σ 𝕜 (↑x : A)), Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
Tactic: by_cases hz' : z ∈ σ 𝕜 (x : A)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 (↑x : A)
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
have this : CompleteSpace.{u_4} ↥S
Tactic: have : CompleteSpace S := hS.completeSpace_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 (↑x : A)
this : CompleteSpace.{u_4} ↥S
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)
have neg : connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z ⊆ σ 𝕜 x
Tactic: suffices connectedComponentIn (σ 𝕜 (x : A))ᶜ z ⊆ σ 𝕜 x from spectrum.isBounded x |>.subset this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
z : 𝕜
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 (↑x : A)
this : CompleteSpace.{u_4} ↥S
⊢ connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z ⊆ σ 𝕜 x
have neg : connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z ⊆
  σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z
Tactic: rw [spectrum_sUnion_connectedComponentIn S]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
h : IsPreconnected (σ 𝕜 (↑x : A))ᶜ
this : σ 𝕜 x \ σ 𝕜 (↑x : A) = ∅
⊢ σ 𝕜 x = σ 𝕜 (↑x : A)
have rw : σ 𝕜 (↑x : A) ∪ ⋃ (z : 𝕜), ⋃ (_ : Membership.mem (γ := Set 𝕜) ∅ z), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z = σ 𝕜 (↑x : A)
Tactic: rw [spectrum_sUnion_connectedComponentIn, this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
h : IsPreconnected (σ 𝕜 (↑x : A))ᶜ
⊢ σ 𝕜 x = σ 𝕜 (↑x : A)
have suffices : σ 𝕜 x \ σ 𝕜 (↑x : A) = ∅
Tactic: suffices σ 𝕜 x \ σ 𝕜 (x : A) = ∅ by
    rw [spectrum_sUnion_connectedComponentIn, this]
    simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
h : IsPreconnected (σ 𝕜 (↑x : A))ᶜ
⊢ σ 𝕜 x \ σ 𝕜 (↑x : A) = ∅
have refine : ∀ (z : 𝕜) (hz : z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A)), Bornology.IsBounded.{u_3} (α := 𝕜) univ
Tactic: refine eq_empty_of_forall_notMem fun z hz ↦ NormedSpace.unbounded_univ 𝕜 𝕜 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
h : IsPreconnected (σ 𝕜 (↑x : A))ᶜ
z : 𝕜
hz : z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A)
⊢ Bornology.IsBounded.{u_3} (α := 𝕜) univ
have hz₁ : z ∈ σ 𝕜 x
Tactic: obtain ⟨hz, hz'⟩ := mem_diff _ |>.mp hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
h : IsPreconnected (σ 𝕜 (↑x : A))ᶜ
z : 𝕜
hz : z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A)
hz₁ : z ∈ σ 𝕜 x
⊢ Bornology.IsBounded.{u_3} (α := 𝕜) univ
have hz' : z ∉ σ 𝕜 (↑x : A)
Tactic: obtain ⟨hz, hz'⟩ := mem_diff _ |>.mp hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
x : ↥S
h : IsPreconnected (σ 𝕜 (↑x : A))ᶜ
z : 𝕜
hz_1 : z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A)
hz : z ∈ σ 𝕜 x
hz' : z ∉ σ 𝕜 (↑x : A)
⊢ Bornology.IsBounded.{u_3} (α := 𝕜) univ
have this : Bornology.IsBounded (σ 𝕜 (↑x : A) ∪ (σ 𝕜 (↑x : A))ᶜ)
Tactic: have := (spectrum.isBounded (x : A)).union <|
    h.connectedComponentIn hz' ▸ spectrum_isBounded_connectedComponentIn S x hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
⊢ Eq (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))
have this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
Tactic: have := algebraMap_isometry 𝕜₁ 𝕜₂ |>.nnnorm_map_of_map_zero (map_zero _)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
⊢ Eq (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))
have a₁ : LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
a₁ : LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))
have a₂ : LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
⊢ LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))
have apply : ∀ (x : 𝕜₁) (hx : x ∈ spectrum 𝕜₁ a), (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)
Tactic: apply iSup₂_le fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
⊢ LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞))
have apply : ∀ (x : 𝕜₂) (hx : x ∈ spectrum 𝕜₂ a), (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
Tactic: apply iSup₂_le fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
x : 𝕜₁
hx : x ∈ spectrum 𝕜₁ a
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)
have refine : Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂)
Tactic: refine congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
x : 𝕜₂
hx : x ∈ spectrum 𝕜₂ a
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
have have : ∀ (y : 𝕜₁) (hy : y ∈ spectrum 𝕜₁ a) (hy' : (algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y = x),
  (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
Tactic: have ⟨y, hy, hy'⟩ := h.algebraMap_image.symm ▸ hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜₁ : Type u_3
𝕜₂ : Type u_4
A : Type u_5
inst : NormedField 𝕜₁
inst_1 : NormedField 𝕜₂
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜₁ A
inst_4 : NormedAlgebra 𝕜₂ A
inst_5 : NormedAlgebra 𝕜₁ 𝕜₂
inst_6 : IsScalarTower 𝕜₁ 𝕜₂ A
f : 𝕜₂ → 𝕜₁
a : A
h : SpectrumRestricts a f
this : ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊
x : 𝕜₂
hx : x ∈ spectrum 𝕜₂ a
y : 𝕜₁
hy : y ∈ spectrum 𝕜₁ a
hy' : (algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y = x
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
have subst : ∀ (hx : Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)),
  (↑(nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)) : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
Tactic: subst hy'
Cleared hypotheses: x, hx, hy'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ x ∈ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
have rw : (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
Tactic: rw [Set.mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe,
      ← ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
have this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
Tactic: have : spectrum ℝ a ⊆ Set.Icc (-t) t := by
    intro x hx
    rw [Set.mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe,
      ← ENNReal.coe_le_coe]
    exact le_iSup₂ (α := ℝ≥0∞) x hx |>.trans ht
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
have rw : (∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔
  spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
Tactic: rw [nnreal_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
⊢ (∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
have refine_1 : ∀ (h : ∀ x ∈ spectrum ℝ a, 0 ≤ x) (x : ℝ)
  (hx : x ∈ spectrum ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
  (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
Tactic: refine ⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
refine_1 :
  ∀ (h : ∀ x ∈ spectrum ℝ a, 0 ≤ x) (x : ℝ)
    (hx : x ∈ spectrum ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
⊢ (∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
have refine_2 : ∀ (h : spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)),
  ∀ x ∈ spectrum ℝ a, 0 ≤ x
Tactic: refine ⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ spectrum ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
have hx₁ : x ∈ {(↑t : ℝ)} - spectrum ℝ a
Tactic: rw [← spectrum.singleton_sub_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ {(↑t : ℝ)} - spectrum ℝ a
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
have refine_1 : ∀ (y : ℝ) (hy : y ∈ spectrum ℝ a) (hx : (↑t : ℝ) - y ∈ {(↑t : ℝ)} - spectrum ℝ a),
  (↑‖(↑t : ℝ) - y‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
Tactic: obtain ⟨y, hy, rfl⟩ : ∃ y ∈ spectrum ℝ a, ↑t - y = x := by simpa using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : (↑t : ℝ) - y ∈ {(↑t : ℝ)} - spectrum ℝ a
⊢ (↑‖(↑t : ℝ) - y‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
have hty : -(↑t : ℝ) ≤ y
Tactic: obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : (↑t : ℝ) - y ∈ {(↑t : ℝ)} - spectrum ℝ a
hty : -(↑t : ℝ) ≤ y
⊢ (↑‖(↑t : ℝ) - y‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
have hyt : y ≤ (↑t : ℝ)
Tactic: obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : (↑t : ℝ) - y ∈ {(↑t : ℝ)} - spectrum ℝ a
hty : -(↑t : ℝ) ≤ y
hyt : y ≤ (↑t : ℝ)
⊢ (↑‖(↑t : ℝ) - y‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
have refine_1 : ∀ (y : ℝ≥0) (hy : (↑y : ℝ) ∈ spectrum ℝ a) (hx : (↑t : ℝ) - (↑y : ℝ) ∈ {(↑t : ℝ)} - spectrum ℝ a)
  (hty : -(↑t : ℝ) ≤ (↑y : ℝ)) (hyt : (↑y : ℝ) ≤ (↑t : ℝ)), (↑‖(↑t : ℝ) - (↑y : ℝ)‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
Tactic: lift y to ℝ≥0 using h y hy
Cleared hypotheses: y, hy, hx, hty, hyt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ≥0
hy : (↑y : ℝ) ∈ spectrum ℝ a
hx : (↑t : ℝ) - (↑y : ℝ) ∈ {(↑t : ℝ)} - spectrum ℝ a
hty : -(↑t : ℝ) ≤ (↑y : ℝ)
hyt : (↑y : ℝ) ≤ (↑t : ℝ)
⊢ (↑‖(↑t : ℝ) - (↑y : ℝ)‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
have refine_1 : (↑‖(↑(t - y) : ℝ)‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
Tactic: rw [← NNReal.coe_sub (by exact_mod_cast hyt)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have h₁ : ∀ x ∈ spectrum ℝ a, ‖(↑t : ℝ) - x‖₊ ≤ t
Tactic: replace h : ∀ x ∈ spectrum ℝ a, ‖t - x‖₊ ≤ t := by
      simpa [spectralRadius, iSup₂_le_iff, ← spectrum.singleton_sub_eq] using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, ‖(↑t : ℝ) - x‖₊ ≤ t
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x
have refine_2 : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (h_le : ‖(↑t : ℝ) - x‖₊ ≤ t), 0 ≤ x
Tactic: peel h with x hx h_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, ‖(↑t : ℝ) - x‖₊ ≤ t
x : ℝ
hx : x ∈ spectrum ℝ a
h_le : ‖(↑t : ℝ) - x‖₊ ≤ t
⊢ 0 ≤ x
have h_le₁ : -(↑t : ℝ) ≤ (↑t : ℝ) - x ∧ (↑t : ℝ) - x ≤ (↑t : ℝ)
Tactic: rw [← NNReal.coe_le_coe, coe_nnnorm, Real.norm_eq_abs, abs_le] at h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : spectrum ℝ a ⊆ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)
h : ∀ x ∈ spectrum ℝ a, ‖(↑t : ℝ) - x‖₊ ≤ t
x : ℝ
hx : x ∈ spectrum ℝ a
h_le : -(↑t : ℝ) ≤ (↑t : ℝ) - x ∧ (↑t : ℝ) - x ≤ (↑t : ℝ)
⊢ 0 ≤ x
have linarith : x < 0 → (↑t : ℝ) - x - (↑t : ℝ) + (x - 0) = 0
Tactic: linarith [h_le.2]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
have obtain : ∀ (x : ℝ) (hx₁ : x ∈ spectrum ℝ a) (hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a),
  (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
Tactic: obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
⊢ (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
have rw : (↑‖x‖₊ : ℝ) ∈ spectrum ℝ a
Tactic: rw [← hx₂, ENNReal.toNNReal_coe, ← spectrum.algebraMap_mem_iff ℝ, NNReal.algebraMap_eq_coe]