mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
z : 𝕜ˣ
hz : ↑z ∈ {0}ᶜ
⊢ resolvent a ↑z = (↑z)⁻¹ • resolvent ((↑z)⁻¹ • a) 1

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
z : 𝕜ˣ
hz : ↑z ∈ {0}ᶜ
⊢ resolvent a ↑z = (↑z)⁻¹ • resolvent ((↑z)⁻¹ • a) 1
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
⊢ (fun z ↦ z⁻¹ • resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ ‖x⁻¹‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
h : (fun z ↦ resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ 1
⊢ (fun z ↦ z⁻¹ • resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x ↦ ‖x‖⁻¹
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
⊢ IsCompact Set.univ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompactSpace α
⊢ IsCompact Set.univ
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
⊢ ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
⊢ ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • ((a - ↑ₐ z) * (a - ↑ₐ z) ^ n) = (a - ↑ₐ z) * b
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
⊢ ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = b * (a - ↑ₐ z)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul : exp a = exp (a - ↑ₐ z) * ↑ₐ (exp z)
b : A := ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
hb : Summable fun n ↦ (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ n
h₀ : ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • (a - ↑ₐ z) ^ (n + 1) = (a - ↑ₐ z) * b
⊢ ∑' (n : ℕ), (↑(n + 1).factorial)⁻¹ • ((a - ↑ₐ z) ^ n * (a - ↑ₐ z)) = b * (a - ↑ₐ z)
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
φ : A →ₐ[𝕜] 𝕜
x✝¹ : ℝ
x✝ : x✝¹ ≥ 0
h : ∀ (x : A), ‖φ.toContinuousLinearMap x‖ ≤ x✝¹ * ‖x‖
⊢ 1 ≤ x✝¹

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : CompleteSpace A
inst✝ : NormOneClass A
φ : A →ₐ[𝕜] 𝕜
x✝¹ : ℝ
x✝ : x✝¹ ≥ 0
h : ∀ (x : A), ‖φ.toContinuousLinearMap x‖ ≤ x✝¹ * ‖x‖
⊢ 1 ≤ x✝¹
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ ↑⋯.unit *
      { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ } ↑hx.unit⁻¹ =
    1

Tactic:
simpa using

Goal state after:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
l : Filter ↥S
a : ↥S
ha : IsUnit ↑a
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S)) l) (𝓝 ↑ha.unit⁻¹)
x : ↥S
hx : IsUnit x
⊢ ↑x * ↑↑hx.unit⁻¹ = 1
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 ↑x

Tactic:
by
  have : CompleteSpace S := hS.completeSpace_coe
  intro μ hμ
  by_contra h
  rw [spectrum.notMem_iff] at h
  rw [← frontier_compl, (spectrum.isClosed _).isOpen_compl.frontier_eq, Set.mem_sdiff] at hμ
  obtain ⟨hμ₁, hμ₂⟩ := hμ
  rw [mem_closure_iff_clusterPt] at hμ₁
  apply hμ₂
  rw [mem_compl_iff, spectrum.notMem_iff]
  refine Subalgebra.isUnit_of_isUnit_val_of_eventually S h ?_ ?_ <| .map hμ₁ (algebraMap 𝕜 S · - x)
  · calc
      _ ≤ map _ (𝓝 μ) := map_mono (by simp)
      _ ≤ _ := by rw [← Filter.Tendsto, ← ContinuousAt]; fun_prop
  · rw [eventually_map]
    apply Eventually.filter_mono inf_le_right
    simp [spectrum.notMem_iff]

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ IsOpen {p | Disjoint p.1 p.2}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ IsOpen {p | Disjoint p.1 p.2}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ ‖(cfcHom ha) { toFun := (σ 𝕜 a).domRestrict f, continuous_toFun := ⋯ }‖ ≤ c

Tactic:
simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.norm_cfc f a hf ha |>.isLUB)]

Goal state after:
case inr
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
hc : 0 ≤ c
h : ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c
h✝ : Nontrivial A
hf : ContinuousOn f (σ 𝕜 a)
ha : p a
⊢ c ∈ upperBounds ((fun x ↦ ‖f x‖) '' σ 𝕜 a)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Dense {K | (↑K).Finite}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ closure {K | (↑K).Finite} = univ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
a : A
ha : p a
⊢ IsGreatest ((fun x ↦ ‖x‖) '' σ 𝕜 a) ‖a‖

Tactic:
by
  simpa only [cfc_id 𝕜 a] using! IsGreatest.norm_cfc (id : 𝕜 → 𝕜) a

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
h₁ : Function.Injective ⇑(codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
⊢ Function.Injective ⇑ψ

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
inst✝² : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst✝¹ : CompleteSpace A
inst✝ : CStarRing A
a : A
ha : p a
ψ : C(↑(σₙ 𝕜 a), 𝕜)₀ →⋆ₙₐ[𝕜] A :=
  (↑(inrRangeEquiv 𝕜 A).symm).comp
    (codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
coe_ψ : ∀ (f : C(↑(σₙ 𝕜 a), 𝕜)₀), ↑(ψ f) = (cfcₙAux ⋯ a ha) f
h₁ : Function.Injective ⇑(codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
⊢ Function.Injective ⇑(codRestrict (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom 𝕜 A)) ⋯)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ S a)
⊢ dist
      (({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
          (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
        x)
      (({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
          (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
        x) ≤
    dist g₁ g₂

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ S a)
⊢ dist (g₁ (Subtype.map ⇑f ⋯ x)) (g₂ (Subtype.map ⇑f ⋯ x)) ≤ dist g₁ g₂
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
this : Set.EqOn (fun x ↦ star (id x)) id (σₙ ℂ a)
⊢ (starRingEnd ℂ) x = x

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsSelfAdjoint a
x : ℂ
hx : x ∈ σₙ ℂ a
this : Set.EqOn (fun x ↦ star (id x)) id (σₙ ℂ a)
⊢ (starRingEnd ℂ) x = x
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
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

Goal state after:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
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
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: case right.left
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ QuasispectrumRestricts (cfcₙ (fun x ↦ √x) a) ⇑ContinuousMap.realToNNReal

Tactic:
simpa using

Goal state after:
case right.left
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module ℝ A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha₁ : IsSelfAdjoint a
ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ ∀ a_1 ∈ σₙ ℝ a, 0 ≤ √a_1
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
⊢ ∀ x ∈ spectrum ℝ a, ‖↑t - x‖₊ ≤ t

Tactic:
simpa using

Goal state after:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
⊢ ∀ x ∈ spectrum ℝ a, ‖↑t - x‖₊ ≤ t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
⊢ ‖0‖ ≤ c

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c
⊢ 0 ≤ c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : A
hx : IsSelfAdjoint x
ha₁ : IsSelfAdjoint (x * x)
ha₂ : QuasispectrumRestricts (x * x) ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ x * x

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : PartialOrder A
inst✝⁷ : StarRing A
inst✝⁶ : StarOrderedRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Module ℝ A
inst✝³ : IsScalarTower ℝ A A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
x : A
hx : IsSelfAdjoint x
ha₁ : IsSelfAdjoint (x * x)
ha₂ : QuasispectrumRestricts (x * x) ⇑ContinuousMap.realToNNReal
⊢ 0 ≤ x * x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric

Goal state before:
pp: case refine_1
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
⊢ ‖0‖ < c

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
c : ℝ
h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c
⊢ 0 < c
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ ‖a - a₀‖ ≤ 1

Tactic:
simpa using

Goal state after:
case h₂
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : ProperSpace 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ ‖a - a₀‖ ≤ 1
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: A : Type u_2
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous (quasispectrum ℝ≥0)

Tactic:
simpa using

Goal state after:
A : Type u_2
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
h₁ : IsInducing NNReal.toReal
⊢ UpperHemicontinuous (quasispectrum ℝ≥0)
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ s ⊆ closure {z | r < z.im}

Tactic:
simpa using

Goal state after:
r : ℝ
s : Set ℂ
hs₁ : {z | r < z.im} ⊆ s
hs₂ : s ⊆ {z | r ≤ z.im}
⊢ s ⊆ {z | r ≤ z.im}
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ s ⊆ closure {z | z.im < r}

Tactic:
simpa using

Goal state after:
r : ℝ
s : Set ℂ
hs₁ : {z | z.im < r} ⊆ s
hs₂ : s ⊆ {z | z.im ≤ r}
⊢ s ⊆ {z | z.im ≤ r}
Module: Mathlib.Analysis.Complex.Convex

Goal state before:
pp: U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ z.Rectangle w ⊆ U

Tactic:
simpa using

Goal state after:
U : Set ℂ
U_convex : Convex ℝ U
z w : ℂ
hz : z ∈ U
hw : w ∈ U
hzw : ↑z.re + ↑w.im * I ∈ U
hwz : ↑w.re + ↑z.im * I ∈ U
⊢ (convexHull ℝ) {z, ↑z.re + ↑w.im * I, ↑w.re + ↑z.im * I, w} ⊆ U
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ ‖k‖ ≤ 1

Tactic:
simpa using

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k ∈ σ 𝕜 ↑u
⊢ ‖k‖ ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ σ 𝕜 ↑(toUnits u)⁻¹
hnk : k ≠ 0
⊢ ‖k‖⁻¹ ≤ ‖↑(toUnits u)⁻¹‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ σ 𝕜 ↑(toUnits u)⁻¹
hnk : k ≠ 0
⊢ ‖k‖⁻¹ ≤ ‖↑(toUnits u)⁻¹‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ σ 𝕜 ↑(toUnits u)⁻¹
hnk : k ≠ 0
this : ‖k‖⁻¹ ≤ ‖↑(toUnits u)⁻¹‖
⊢ 1 ≤ ‖k‖

Tactic:
simpa using

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : ↥(unitary E)
a✝ : Nontrivial E
k : 𝕜
hk : k⁻¹ ∈ σ 𝕜 ↑(toUnits u)⁻¹
hnk : k ≠ 0
this : ‖k‖⁻¹ ≤ ‖↑(toUnits u)⁻¹‖
⊢ 1 ≤ ‖k‖
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : E
hu : u ∈ unitary E
z : 𝕜
hz : z ∈ σ 𝕜 u
⊢ ‖z‖ = 1

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NormedField 𝕜
E : Type u_2
inst✝⁴ : NormedRing E
inst✝³ : StarRing E
inst✝² : CStarRing E
inst✝¹ : NormedAlgebra 𝕜 E
inst✝ : CompleteSpace E
u : E
hu : u ∈ unitary E
z : 𝕜
hz : z ∈ σ 𝕜 u
⊢ ‖z‖ = 1
Module: Mathlib.Analysis.CStarAlgebra.Spectrum

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 ↑a
⊢ x ≤ ‖a‖₊

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
x : ℝ≥0
hx : x ∈ σ ℝ≥0 ↑a
⊢ x ≤ ‖a‖₊
Module: Mathlib.Analysis.Normed.Algebra.GelfandFormula

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ ‖z‖₊ ≤ r

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : CompleteSpace A
a : A
r : ℝ≥0
hr : ↑r < (spectralRadius 𝕜 a)⁻¹
z : 𝕜
z_mem : z ∈ Metric.closedBall 0 ↑r
⊢ ‖z‖₊ ≤ r