awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ)
⊢ (↑‖(↑(t - y) : ℝ)‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)

Tactic:
simp
-- 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 : spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
⊢ ∀ x ∈ spectrum ℝ a, ‖(↑t : ℝ) - x‖₊ ≤ t

Tactic:
simpa [spectralRadius, iSup₂_le_iff, ← spectrum.singleton_sub_eq] using h

Premises used: spectralRadius, spectrum.singleton_sub_eq, iSup₂_le_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 : ℝ)
h : spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
⊢ ∀ 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
-- 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, ‖(↑t : ℝ) - x‖₊ ≤ t
refine_2 : ∀ (x : ℝ) (hx : x ∈ spectrum ℝ a) (h_le : ‖(↑t : ℝ) - x‖₊ ≤ t), 0 ≤ x
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
peel h with x hx h_le
-- 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, ‖(↑t : ℝ) - x‖₊ ≤ t
x : ℝ
hx : x ∈ spectrum ℝ a
h_le : ‖(↑t : ℝ) - x‖₊ ≤ t
⊢ -(↑t : ℝ) ≤ (↑t : ℝ) - x ∧ (↑t : ℝ) - x ≤ (↑t : ℝ)

Tactic:
rw [← NNReal.coe_le_coe, coe_nnnorm, Real.norm_eq_abs, abs_le] at h_le

Premises used: abs_le, coe_nnnorm, 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∞)
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 : ℝ)
linarith : x < 0 → (↑t : ℝ) - x - (↑t : ℝ) + (x - 0) = 0
⊢ 0 ≤ x

Tactic:
linarith [h_le.2]

Premises used: And.right
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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)
obtain :
  ∀ (x : ℝ) (hx₁ : x ∈ spectrum ℝ a) (hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a),
    (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a
⊢ (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha

Premises used: spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
rw : (↑‖x‖₊ : ℝ) ∈ spectrum ℝ a
⊢ (spectralRadius ℝ a).toNNReal ∈ spectrum ℝ≥0 a

Tactic:
rw [← hx₂, ENNReal.toNNReal_coe, ← spectrum.algebraMap_mem_iff ℝ, NNReal.algebraMap_eq_coe]

Premises used: Real, NNReal.algebraMap_eq_coe, ENNReal.toNNReal_coe, spectrum.algebraMap_mem_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
⊢ 0 ≤ x

Tactic:
have : 0 ≤ x := ha'.rightInvOn hx₁ ▸ NNReal.zero_le_coe
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
this : 0 ≤ x
⊢ x ∈ spectrum ℝ a

Tactic:
hx₁
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
this : 0 ≤ x
h : (↑‖x‖₊ : ℝ) = x
⊢ (↑‖x‖₊ : ℝ) ∈ spectrum ℝ a

Tactic:
convert! hx₁
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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
this : 0 ≤ x
⊢ (↑‖x‖₊ : ℝ) = x

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
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).toReal ∈ spectrum ℝ a

Tactic:
NNReal.spectralRadius_mem_spectrum ha ha'

Premises used: spectrum, Set.Mem, setOf, NNReal, NNReal.spectralRadius_mem_spectrum, ENNReal.toReal, resolventSet, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
obtain :
  ∀ (x : ℝ) (hx₁ : x ∈ spectrum ℝ a) (hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a),
    (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha

Premises used: spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
simp : |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
simp only [← hx₂, ENNReal.coe_toReal, coe_nnnorm, Real.norm_eq_abs]

Premises used: ENNReal.coe_toReal, coe_nnnorm, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
h : |x| = x
rwa rwa₁ rwa₂ rwa₃ : x ∈ spectrum ℝ a
⊢ |x| ∈ spectrum ℝ a

Tactic:
rwa [h]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
h : |x| = -x
⊢ -|x| ∈ spectrum ℝ a

Tactic:
simpa [h]
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
⊢ |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a

Tactic:
exact abs_choice x |>.imp (fun h ↦ by rwa [h]) (fun h ↦ by simpa [h])

Premises used: abs_choice, Or.imp
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
inst_9 : TopologicalSpace R
inst_10 : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts.{u_3, u_4, u_5} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : CompactSpace.{u_4} (↑(σₙ S a) : Type u_4)
rw : ∀ (h_cpct : IsCompact (σₙ S a)), IsCompact (σₙ R a)
⊢ CompactSpace.{u_3} (↑(σₙ R a) : Type u_3)

Tactic:
rw [← isCompact_iff_compactSpace] at h_cpct ⊢

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
inst_9 : TopologicalSpace R
inst_10 : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts.{u_3, u_4, u_5} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : IsCompact (σₙ S a)
⊢ IsCompact (σₙ R a)

Tactic:
h.image ▸ h_cpct.image (map_continuous f)

Premises used: Eq.rec, QuasispectrumRestricts.image, ContinuousMapClass.map_continuous, IsCompact.image
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
inst_9 : TopologicalSpace R
inst_10 : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts.{u_3, u_4, u_5} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : IsCompact (σₙ S a)
⊢ IsCompact (σₙ R a)

Tactic:
exact h.image ▸ h_cpct.image (map_continuous f)
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
⊢ ∀ (x : A), UpperHemicontinuousAt (spectrum 𝕜) x

Tactic:
fun a₀ ↦ .of_sequences
    (isCompact_closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)).isSeqCompact ?_ <|
    fun a ha x hx_mem x₀ hx ↦ ?_

Premises used: Norm.norm, HMul.hMul, UpperHemicontinuousAt.of_sequences, HAdd.hAdd, ProperSpace.isCompact_closedBall, OfNat.ofNat, IsCompact.isSeqCompact
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
refine_1 : ∀ (a₀ : A), ∀ᶠ (x : A) in 𝓝 a₀, spectrum 𝕜 x ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
refine_2 :
  ∀ (a₀ : A) (a : ℕ → A) (ha : Tendsto a atTop (𝓝 a₀)) (x : ℕ → 𝕜) (hx_mem : ∀ (n : ℕ), x n ∈ spectrum 𝕜 (a n)) (x₀ : 𝕜)
    (hx : Tendsto x atTop (𝓝 x₀)), x₀ ∈ spectrum 𝕜 a₀
⊢ ∀ (x : A), UpperHemicontinuousAt (spectrum 𝕜) x

Tactic:
refine fun a₀ ↦ .of_sequences
    (isCompact_closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)).isSeqCompact ?_ <|
    fun a ha x hx_mem x₀ hx ↦ ?_
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ : A
h : ∀ (a : A) (ha : a ∈ Metric.closedBall a₀ 1), spectrum 𝕜 a ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
⊢ ∀ᶠ (x : A) in 𝓝 a₀, spectrum 𝕜 x ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)

Tactic:
filter_upwards [Metric.closedBall_mem_nhds a₀ zero_lt_one] with a ha

Premises used: Metric.closedBall_mem_nhds, zero_lt_one
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
apply : ‖a‖ * norm.{u_2} (E := A) 1 ≤ (‖a₀‖ + 1) * norm.{u_2} (E := A) 1
⊢ spectrum 𝕜 a ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)

Tactic:
apply spectrum.subset_closedBall_norm_mul a |>.trans <| Metric.closedBall_subset_closedBall ?_

Premises used: spectrum.subset_closedBall_norm_mul, HasSubset.Subset.trans, Metric.closedBall_subset_closedBall
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
hbc : ‖a‖ ≤ ‖a₀‖ + 1
⊢ ‖a‖ * norm.{u_2} (E := A) 1 ≤ (‖a₀‖ + 1) * norm.{u_2} (E := A) 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
hbc : ‖a₀‖ + ‖a - a₀‖ ≤ ‖a₀‖ + 1
⊢ ‖a‖ ≤ ‖a₀‖ + 1

Tactic:
apply norm_le_norm_add_norm_sub' a a₀ |>.trans

Premises used: norm_le_norm_add_norm_sub', LE.le.trans
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
hbc : ‖a - a₀‖ ≤ 1
⊢ ‖a₀‖ + ‖a - a₀‖ ≤ ‖a₀‖ + 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ ‖a - a₀‖ ≤ 1

Tactic:
simpa [dist_eq_norm] using ha

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ : A
a : ℕ → A
ha : Tendsto a atTop (𝓝 a₀)
x : ℕ → 𝕜
hx_mem : ∀ (n : ℕ), x n ∈ spectrum 𝕜 (a n)
x₀ : 𝕜
hx : Tendsto x atTop (𝓝 x₀)
⊢ x₀ ∈ spectrum 𝕜 a₀

Tactic:
nonunits.isClosed.mem_of_tendsto
      (continuous_algebraMap 𝕜 A |>.tendsto x₀ |>.comp hx |>.sub ha) <| .of_forall hx_mem

Premises used: spectrum, Set.Mem, setOf, continuous_algebraMap, IsUnit, nonunits, nonunits.isClosed, IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Continuous.tendsto, resolventSet, Filter.Tendsto.comp, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ : A
a : ℕ → A
ha : Tendsto a atTop (𝓝 a₀)
x : ℕ → 𝕜
hx_mem : ∀ (n : ℕ), x n ∈ spectrum 𝕜 (a n)
x₀ : 𝕜
hx : Tendsto x atTop (𝓝 x₀)
⊢ x₀ ∈ spectrum 𝕜 a₀

Tactic:
exact nonunits.isClosed.mem_of_tendsto
      (continuous_algebraMap 𝕜 A |>.tendsto x₀ |>.comp hx |>.sub ha) <| .of_forall hx_mem

Premises used: continuous_algebraMap, nonunits.isClosed, IsClosed.mem_of_tendsto, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
⊢ IsClosedEmbedding NNReal.toReal

Tactic:
NNReal.isClosedEmbedding_coe

Premises used: NNReal.isClosedEmbedding_coe
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
⊢ IsClosed (range NNReal.toReal)

Tactic:
obtain ⟨⟨h₁, -⟩, h₂⟩ : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := NNReal.isClosedEmbedding_coe

Premises used: NNReal.isClosedEmbedding_coe, NNReal.toReal, Topology.IsClosedEmbedding
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
⊢ IsInducing NNReal.toReal

Tactic:
obtain ⟨⟨h₁, -⟩, h₂⟩ : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := NNReal.isClosedEmbedding_coe

Premises used: NNReal.isClosedEmbedding_coe, NNReal.toReal, Topology.IsClosedEmbedding
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (spectrum ℝ≥0)

Tactic:
upperHemicontinuous_spectrum ℝ A |>.isInducing_comp h₁ h₂

Premises used: Real, spectrum, Set.Mem, setOf, NNReal, Set.preimage, resolventSet, UpperHemicontinuous.isInducing_comp, Not, upperHemicontinuous_spectrum
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (spectrum ℝ≥0)

Tactic:
exact upperHemicontinuous_spectrum ℝ A |>.isInducing_comp h₁ h₂

Premises used: Real, UpperHemicontinuous.isInducing_comp, upperHemicontinuous_spectrum
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
⊢ UpperHemicontinuous.{u_2, u_1} (α := A)
    (Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A))

Tactic:
upperHemicontinuous_spectrum 𝕜 (WithLp 1 (Unitization 𝕜 A)) |>.comp
      unitization_isometry_inr.continuous

Premises used: WithLp, Isometry.continuous, UpperHemicontinuous.comp, Unitization, OfNat.ofNat, upperHemicontinuous_spectrum, WithLp.unitization_isometry_inr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
h :
  Eq (α := A → Set 𝕜) (quasispectrum 𝕜)
    (Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A))
⊢ UpperHemicontinuous.{u_2, u_1} (α := A) (quasispectrum 𝕜)

Tactic:
convert!
    upperHemicontinuous_spectrum 𝕜 (WithLp 1 (Unitization 𝕜 A)) |>.comp
      unitization_isometry_inr.continuous

Premises used: WithLp, Isometry.continuous, UpperHemicontinuous.comp, Unitization, OfNat.ofNat, upperHemicontinuous_spectrum, WithLp.unitization_isometry_inr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
h :
  ∀ (a : A),
    quasispectrum 𝕜 a =
      Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a
⊢ Eq (α := A → Set 𝕜) (quasispectrum 𝕜)
    (Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A))

Tactic:
ext1 a
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
a : A
h :
  spectrum 𝕜 (A := WithLp 1 (Unitization 𝕜 A))
      ((AlgEquiv.symm (unitizationAlgEquiv 𝕜) : (a : Unitization 𝕜 A) → WithLp 1 (Unitization 𝕜 A))
          (↑a : Unitization 𝕜 A) :
        WithLp 1 (Unitization 𝕜 A)) =
    Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a
⊢ quasispectrum 𝕜 a =
    Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a

Tactic:
rw [Unitization.quasispectrum_eq_spectrum_inr,
    ← AlgEquiv.spectrum_eq (unitizationAlgEquiv 𝕜 (𝕜 := 𝕜) (A := A) |>.symm)]

Premises used: WithLp.unitizationAlgEquiv, AlgEquiv.symm, AlgEquiv.spectrum_eq, Unitization.quasispectrum_eq_spectrum_inr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
a : A
⊢ spectrum 𝕜 (A := WithLp 1 (Unitization 𝕜 A))
      ((AlgEquiv.symm (unitizationAlgEquiv 𝕜) : (a : Unitization 𝕜 A) → WithLp 1 (Unitization 𝕜 A))
          (↑a : Unitization 𝕜 A) :
        WithLp 1 (Unitization 𝕜 A)) =
    Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : CompleteSpace A
⊢ IsClosed (range NNReal.toReal)

Tactic:
obtain ⟨⟨h₁, -⟩, h₂⟩ := NNReal.isClosedEmbedding_coe

Premises used: NNReal.isClosedEmbedding_coe
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
⊢ IsInducing NNReal.toReal

Tactic:
obtain ⟨⟨h₁, -⟩, h₂⟩ := NNReal.isClosedEmbedding_coe

Premises used: NNReal.isClosedEmbedding_coe
-- Module: Mathlib.Analysis.Normed.Algebra.Spectrum
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (quasispectrum ℝ≥0)

Tactic:
simpa [← NNReal.algebraMap_eq_coe] using
    upperHemicontinuous_quasispectrum ℝ A |>.isInducing_comp h₁ h₂

Premises used: Real, NNReal.algebraMap_eq_coe, upperHemicontinuous_quasispectrum, UpperHemicontinuous.isInducing_comp
-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Algebra 𝕜 R
inst_4 : Module 𝕜 M
inst_5 : Module R M
inst_6 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_7 : SMulCommClass R Rᵐᵒᵖ M
inst_8 : IsScalarTower 𝕜 R M
inst_9 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_10 : TopologicalSpace R
inst_11 : TopologicalSpace M
inst_12 : IsTopologicalRing R
inst_13 : IsTopologicalAddGroup M
inst_14 : ContinuousSMul R M
inst_15 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
n : ℕ
⊢ Eq (α := R)
    (fst.{u_3, u_4} (M := M)
        ((expSeries 𝕜 (tsze R M) n : (a : (i : Fin n) → tsze R M) → tsze R M) fun (x_1 : Fin n) ↦ x) :
      R)
    ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R)

Tactic:
simp [expSeries_apply_eq]

Premises used: NormedSpace.expSeries_apply_eq