awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
neg : connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z ⊆ σ 𝕜 x
⊢ Bornology.IsBounded (connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z)

Tactic:
suffices connectedComponentIn (σ 𝕜 (x : A))ᶜ z ⊆ σ 𝕜 x from spectrum.isBounded x |>.subset this
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
neg :
  connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z ⊆
    σ 𝕜 (↑x : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z
⊢ connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z ⊆ σ 𝕜 x

Tactic:
rw [spectrum_sUnion_connectedComponentIn S]

Premises used: Subalgebra.spectrum_sUnion_connectedComponentIn
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z

Tactic:
subset_biUnion_of_mem (mem_diff_of_mem hz hz') |>.trans subset_union_right

Premises used: Set.subset_union_right, Set.subset_biUnion_of_mem, HasSubset.Subset.trans, Set.mem_diff_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : A) ∪ ⋃ z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z

Tactic:
exact subset_biUnion_of_mem (mem_diff_of_mem hz hz') |>.trans subset_union_right

Premises used: Set.subset_union_right, Set.subset_biUnion_of_mem, HasSubset.Subset.trans, Set.mem_diff_of_mem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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) = ∅
rw :
  σ 𝕜 (↑x : A) ∪ ⋃ (z : 𝕜), ⋃ (_ : Membership.mem (γ := Set 𝕜) ∅ z), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z =
    σ 𝕜 (↑x : A)
⊢ σ 𝕜 x = σ 𝕜 (↑x : A)

Tactic:
rw [spectrum_sUnion_connectedComponentIn, this]

Premises used: Subalgebra.spectrum_sUnion_connectedComponentIn
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : A) ∪ ⋃ (z : 𝕜), ⋃ (_ : Membership.mem (γ := Set 𝕜) ∅ z), connectedComponentIn (σ 𝕜 (↑x : A))ᶜ z =
    σ 𝕜 (↑x : A)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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))ᶜ
suffices : σ 𝕜 x \ σ 𝕜 (↑x : A) = ∅
⊢ σ 𝕜 x = σ 𝕜 (↑x : A)

Tactic:
suffices σ 𝕜 x \ σ 𝕜 (x : A) = ∅ by
    rw [spectrum_sUnion_connectedComponentIn, this]
    simp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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) = ∅

Tactic:
eq_empty_of_forall_notMem fun z hz ↦ NormedSpace.unbounded_univ 𝕜 𝕜 ?_

Premises used: NormedSpace.unbounded_univ, Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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))ᶜ
refine : ∀ (z : 𝕜) (hz : z ∈ σ 𝕜 x \ σ 𝕜 (↑x : A)), Bornology.IsBounded.{u_3} (α := 𝕜) univ
⊢ σ 𝕜 x \ σ 𝕜 (↑x : A) = ∅

Tactic:
refine eq_empty_of_forall_notMem fun z hz ↦ NormedSpace.unbounded_univ 𝕜 𝕜 ?_

Premises used: NormedSpace.unbounded_univ, Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
⊢ z ∈ σ 𝕜 x

Tactic:
obtain ⟨hz, hz'⟩ := mem_diff _ |>.mp hz

Premises used: Set.mem_diff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ z ∉ σ 𝕜 (↑x : A)

Tactic:
obtain ⟨hz, hz'⟩ := mem_diff _ |>.mp hz

Premises used: Set.mem_diff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 (σ 𝕜 (↑x : A) ∪ (σ 𝕜 (↑x : A))ᶜ)

Tactic:
have := (spectrum.isBounded (x : A)).union <|
    h.connectedComponentIn hz' ▸ spectrum_isBounded_connectedComponentIn S x hz
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
this : Bornology.IsBounded (σ 𝕜 (↑x : A) ∪ (σ 𝕜 (↑x : A))ᶜ)
⊢ Bornology.IsBounded.{u_3} (α := 𝕜) univ

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ ∀ (x : 𝕜₁), nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂) = ‖x‖₊

Tactic:
have := algebraMap_isometry 𝕜₁ 𝕜₂ |>.nnnorm_map_of_map_zero (map_zero _)
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞))
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∞))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊
apply : ∀ (x : 𝕜₁) (hx : x ∈ spectrum 𝕜₁ a), (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞))

Tactic:
apply iSup₂_le fun x hx ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊
apply : ∀ (x : 𝕜₂) (hx : x ∈ spectrum 𝕜₂ a), (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)) (⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞))

Tactic:
apply iSup₂_le fun x hx ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)

Tactic:
congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_

Premises used: ENNReal.ofNNReal, le_iSup₂, Eq.trans_le, congr_arg, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
refine : Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂)
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₂ a, (↑‖k‖₊ : ℝ≥0∞)

Tactic:
refine congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (this x) |>.symm.trans_le <| le_iSup₂ (α := ℝ≥0∞) _ ?_

Premises used: ENNReal.ofNNReal, le_iSup₂, Eq.trans_le, congr_arg, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂)

Tactic:
(spectrum.algebraMap_mem_iff _).mpr hx

Premises used: Iff.mpr, Set.Mem, spectrum.algebraMap_mem_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) x : 𝕜₂)

Tactic:
exact (spectrum.algebraMap_mem_iff _).mpr hx

Premises used: Iff.mpr, spectrum.algebraMap_mem_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
have :
  ∀ (y : 𝕜₁) (hy : y ∈ spectrum 𝕜₁ a) (hy' : (algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y = x),
    (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)

Tactic:
have ⟨y, hy, hy'⟩ := h.algebraMap_image.symm ▸ hx
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
subst :
  ∀ (hx : Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)),
    (↑(nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)) : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)

Tactic:
subst hy'
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊
y : 𝕜₁
hy : y ∈ spectrum 𝕜₁ a
hx : Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)
⊢ (↑(nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)) : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)

Tactic:
this y ▸ le_iSup₂ (α := ℝ≥0∞) y hy

Premises used: le_iSup₂, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊
y : 𝕜₁
hy : y ∈ spectrum 𝕜₁ a
hx : Membership.mem (α := 𝕜₂) (spectrum 𝕜₂ a) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)
⊢ (↑(nnnorm.{u_4} (E := 𝕜₂) ((algebraMap 𝕜₁ 𝕜₂ : (a : 𝕜₁) → 𝕜₂) y : 𝕜₂)) : ℝ≥0∞) ≤ ⨆ k ∈ spectrum 𝕜₁ a, (↑‖k‖₊ : ℝ≥0∞)

Tactic:
exact this y ▸ le_iSup₂ (α := ℝ≥0∞) y hy
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
rw : (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
⊢ x ∈ Set.Icc (-(↑t : ℝ)) (↑t : ℝ)

Tactic:
rw [Set.mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe,
      ← ENNReal.coe_le_coe]

Premises used: abs_le, ENNReal.coe_le_coe, coe_nnnorm, Set.mem_Icc, NNReal.coe_le_coe, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)

Tactic:
le_iSup₂ (α := ℝ≥0∞) x hx |>.trans ht

Premises used: le_iSup₂, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) x hx |>.trans ht

Premises used: le_iSup₂, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_3
inst : Ring A
inst_1 : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
⊢ 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
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℝ)
rw :
  (∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) 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∞)

Tactic:
rw [nnreal_iff]

Premises used: SpectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)

Tactic:
⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩

Premises used: iSup₂_le, Iff.intro
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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∞)
refine_2 :
  ∀ (h : spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)),
    ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ (∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)

Tactic:
refine ⟨fun h ↦ iSup₂_le fun x hx ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 ∈ {(↑t : ℝ)} - spectrum ℝ a

Tactic:
rw [← spectrum.singleton_sub_eq] at hx

Premises used: spectrum.singleton_sub_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ ∃ y ∈ spectrum ℝ a, (↑t : ℝ) - y = x

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
refine_1 :
  ∀ (y : ℝ) (hy : y ∈ spectrum ℝ a) (hx : (↑t : ℝ) - y ∈ {(↑t : ℝ)} - spectrum ℝ a),
    (↑‖(↑t : ℝ) - y‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
⊢ (↑‖x‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)

Tactic:
obtain ⟨y, hy, rfl⟩ : ∃ y ∈ spectrum ℝ a, ↑t - y = x := by simpa using hx

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

Tactic:
obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy

Premises used: Iff.mp, Set.mem_Icc
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ y ≤ (↑t : ℝ)

Tactic:
obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy

Premises used: Iff.mp, Set.mem_Icc
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℝ)
⊢ 0 ≤ y

Tactic:
h y hy
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℝ)
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∞)
⊢ (↑‖(↑t : ℝ) - y‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)

Tactic:
lift y to ℝ≥0 using h y hy
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℝ)
⊢ y ≤ t

Tactic:
exact_mod_cast hyt
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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 : ℝ)
refine_1 : (↑‖(↑(t - y) : ℝ)‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
⊢ (↑‖(↑t : ℝ) - (↑y : ℝ)‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)

Tactic:
rw [← NNReal.coe_sub (by exact_mod_cast hyt)]

Premises used: NNReal.coe_sub