mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : φ (ContinuousMapZero.id s) * a = 0
hmul_star_id : φ (star (ContinuousMapZero.id s)) * a = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
⊢ φ f * a = 0

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with

Goal state after:
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalSemiring A
inst✝⁷ : Star A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : SeparatelyContinuousMul A
inst✝⁴ : T2Space A
inst✝³ : DistribMulAction 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
s : Set 𝕜
inst✝¹ : Fact (0 ∈ s)
inst✝ : CompactSpace ↑s
φ : C(↑s, 𝕜)₀ →⋆ₙₐ[𝕜] A
a : A
hmul_id : a * φ (ContinuousMapZero.id s) = 0
hmul_star_id : a * φ (star (ContinuousMapZero.id s)) = 0
hφ : Continuous ⇑φ
f : C(↑s, 𝕜)₀
⊢ a * φ f = 0

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
x : α
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuousAt f x ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
by
  simpa [upperHemicontinuousWithinAt_univ_iff] using
    upperHemicontinuousWithinAt_iff_preimage_Iic (s := univ)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → Set β
s : Set α
hf : UpperHemicontinuousOn f s
hg : UpperHemicontinuousOn g s
⊢ UpperHemicontinuousOn (fun x ↦ f x ∪ g x) s

Tactic:
rw [upperHemicontinuousOn_iff] at hf hg ⊢
  exact fun x hx ↦ (hf x hx).union (hg x hx)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
hfx : ∀ (n : ℕ), (f (x n) ∩ t).Nonempty
⊢ (f x₀ ∩ t).Nonempty

Tactic:
choose y hy using hfx

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → Set β
x₀ : α
inst✝ : (𝓝 x₀).IsCountablyGenerated
K : Set β
hK : IsSeqCompact K
hf : ∀ᶠ (x : α) in 𝓝 x₀, f x ⊆ K
h :
  ∀ (x : ℕ → α),
    Tendsto x atTop (𝓝 x₀) → ∀ (y : ℕ → β), (∀ (n : ℕ), y n ∈ f (x n)) → ∀ (y₀ : β), Tendsto y atTop (𝓝 y₀) → y₀ ∈ f x₀
t : Set β
ht : IsClosed[inst✝¹] t
hft : ∃ᶠ (x' : α) in 𝓝 x₀, (f x' ∩ t).Nonempty
x : ℕ → α
hx : Tendsto x atTop (𝓝 x₀)
y : ℕ → β
hy : ∀ (n : ℕ), y n ∈ f (x n) ∩ t
⊢ (f x₀ ∩ t).Nonempty
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ 𝓟 SetRel.id ≤ (𝓤 α).lift' hausdorffEntourage

Tactic:
simp_rw [Filter.principal_le_lift', SetRel.id_subset_iff]
      intro (U : SetRel α α) hU
      have := isRefl_of_mem_uniformity hU
      exact isRefl_hausdorffEntourage U

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
⊢ spectralRadius 𝕜 a ^ n ≤ spectralRadius 𝕜 (a ^ n)

Tactic:
simp only [spectralRadius, ENNReal.iSup₂_pow_of_ne_zero _ hn]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
hn : n ≠ 0
⊢ ⨆ i ∈ σ a, ↑‖i‖₊ ^ n ≤ ⨆ k ∈ σ (a ^ n), ↑‖k‖₊
Module: Mathlib.Analysis.Normed.Algebra.Spectrum

Goal state before:
pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ IsUnit (u⁻¹ • 1 - a)

Tactic:
Units.smul_def,

Goal state after:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
a : A
z : 𝕜
h : ↑‖z‖₊ < (spectralRadius 𝕜 a)⁻¹
hz : ¬z = 0
u : 𝕜ˣ := Units.mk0 z hz
⊢ IsUnit (↑u⁻¹ • 1 - a)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
⊢ CompleteSpace (NonemptyCompacts α) ↔ CompleteSpace α

Tactic:
by
  refine ⟨fun _ => ⟨fun {f} hf => ?_⟩, fun _ => inferInstance⟩
  obtain ⟨K, hK⟩ := CompleteSpace.complete <| hf.map uniformContinuous_singleton
  obtain ⟨x, hx⟩ := K.nonempty
  exists x
  rw [(nhds_basis_opens x).ge_iff]
  intro U ⟨hxU, hU⟩
  filter_upwards [hK <| (isOpen_inter_nonempty_of_isOpen hU).mem_nhds ⟨x, hx, hxU⟩]
  simp

Goal state after:
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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
x : ↥S
h : IsPreconnected (σ 𝕜 ↑x)ᶜ
this : σ 𝕜 x \ σ 𝕜 ↑x = ∅
⊢ σ 𝕜 x = σ 𝕜 ↑x

Tactic:
rw [spectrum_sUnion_connectedComponentIn, this]
    simp

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

Goal state before:
pp: A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (fun x ↦ ↑(f x.toNNReal)) a‖₊

Tactic:
← SpectrumRestricts

Goal state after:
A : Type u_1
inst✝⁷ : NormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedAlgebra ℝ A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : Nontrivial A
f : ℝ≥0 → ℝ≥0
a : A
hf : ContinuousOn f (σ ℝ≥0 a)
ha : 0 ≤ a
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ IsGreatest (f '' σ ℝ≥0 a) ‖cfc (fun x ↦ ↑(f x.toNNReal)) a‖₊
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact {L | ↑L ⊆ K}

Tactic:
isEmbedding_coe.isCompact_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact (SetLike.coe '' {L | ↑L ⊆ K})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
⊢ IsCompact {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}

Tactic:
isEmbedding_coe.isCompact_iff

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst✝³] U
hKu₁ : ↑K ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, (↑K ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : ↑K ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : Set α → Set α
hM : ∀ U ∈ u, IsCompact (M U)
hML : ∀ U ∈ u, M U ⊆ L
hMU : ∀ U ∈ u, M U ⊆ U
hMK : ∀ U ∈ u, (↑K ∩ interior (M U)).Nonempty
⊢ IsCompact (SetLike.coe '' {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty})
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ IsPreconnected (toCompacts '' {K | ↑K ⊆ s})

Tactic:
convert Compacts.isPreconnected_nonempty_subsets hs

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
⊢ toCompacts '' {K | ↑K ⊆ s} = {K | (↑K).Nonempty ∧ ↑K ⊆ s}
Module: Mathlib.Analysis.Normed.Operator.Completeness

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedAddCommGroup Fₗ
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f✝ g✝ : E →SL[σ₁₂] F
E' : Type u_6
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : RingHomIsometric σ₁₂
f : E' → F
s : Set (E' →SL[σ₁₂] F)
hs : Bornology.IsBounded s
hf : f ∈ closure[Pi.topologicalSpace] (DFunLike.coe '' s)
C : ℝ
hC : ∀ x ∈ s, ‖x‖ ≤ C
this : ∀ (x : E'), IsClosed[Pi.topologicalSpace] {g | ‖g x‖ ≤ C * ‖x‖}
x : E'
g : E' →SL[σ₁₂] F
hg : g ∈ s
⊢ g ∈ DFunLike.coe ⁻¹' {g | ‖g x‖ ≤ C * ‖x‖}

Tactic:
exact g.le_of_opNorm_le (hC _ hg) _

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ approx n c.right.left x ≤ approx n c.left x

Tactic:
apply approx_le_approx_of_U_sub_C

Goal state after:
case succ.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ c.left.U ⊆ c.right.left.C
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ approx n c.right x ≤ approx n c.left.right x

Tactic:
apply approx_le_approx_of_U_sub_C

Goal state after:
case succ.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ∈ Icc (approx n c.right x) (approx n c.left x)
c : CU P
⊢ c.left.right.U ⊆ c.right.C
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜✝ : Type u_1
M : Type u_2
E✝ : Type u_3
inst✝¹⁵ : NontriviallyNormedField 𝕜✝
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : TopologicalSpace M
inst✝¹² : Module 𝕜✝ M
inst✝¹¹ : SeminormedAddCommGroup E✝
inst✝¹⁰ : NormedSpace 𝕜✝ E✝
α : Type u_4
𝕜 : Type u_5
E : Type u_6
F : Type u_7
inst✝⁹ : TopologicalSpace α
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
x : F
⊢ Continuous fun a ↦ re (((↑(toStrongDual ≪≫ₗ extendRCLikeₗ ≪≫ₗ LinearEquiv.restrictScalars ℝ toWeakDual)).toFun a) x)

Tactic:
by
    simpa [extendRCLikeₗ_apply] using eval_continuous x

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Ideals

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
this : ∃ g', (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t, 0 < g' x
⊢ ∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t

Tactic:
obtain ⟨g', hI', hgt'⟩ := this

Goal state after:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g' : C(X, ℝ≥0)
hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I
hgt' : ∀ x ∈ t, 0 < g' x
⊢ ∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
⊢ Isometry ⇑(gelfandTransform ℂ A)

Tactic:
refine AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a => ?_
  /- By `spectrum.gelfandTransform_eq`, the spectra of `star a * a` and its
    `gelfandTransform` coincide. Therefore, so do their spectral radii, and since they are
    self-adjoint, so also do their norms. Applying the C⋆-property of the norm and taking square
    roots shows that the norm is preserved. -/
  have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
    unfold spectralRadius; rw [spectrum.gelfandTransform_eq]
  rw [map_mul, (IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
    (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this
  simp only [ENNReal.coe_inj, CStarRing.nnnorm_star_mul_self, ← sq] at this
  simpa only [Function.comp_apply, NNReal.sqrt_sq] using!
    congr_arg (((↑) : ℝ≥0 → ℝ) ∘ ⇑NNReal.sqrt) this

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  let __Subalgebra := (gelfandTransform ℂ A).range;
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
⊢ rng = ⊤

Tactic:
have h : rng.topologicalClosure = rng := le_antisymm
    (StarSubalgebra.topologicalClosure_minimal le_rfl
      (gelfandTransform_isometry A).isClosedEmbedding.isClosed_range)
    (StarSubalgebra.le_topologicalClosure _)

Goal state after:
A : Type u_1
inst✝ : CommCStarAlgebra A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  let __Subalgebra := (gelfandTransform ℂ A).range;
  { toSubalgebra := __Subalgebra, star_mem' := ⋯ }
h : rng.topologicalClosure = rng
⊢ rng = ⊤
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case e'_17
A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x✝ : ℝ
⊢ x✝⁺ - x✝⁻ = id x✝

Tactic:
exact _root_.posPart_sub_negPart _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: case pos
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ≥0
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
⊢ (↑r • x)⁺ = ↑r • x⁺

Tactic:
simp [_root_.posPart_def, mul_max_of_nonneg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a ^ 2 = a

Tactic:
rw [pow_two, sqrt_mul_sqrt_self (A := A) a]

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

Goal state before:
pp: 𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : ContinuousStar A
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
x : ↑{a | p a ∧ spectrum 𝕜 a ⊆ s}
⊢ {a | p a ∧ spectrum 𝕜 a ⊆ s}.domRestrict (cfc f) x =
    (cfcHomSuperset ⋯ ⋯) { toFun := s.domRestrict f, continuous_toFun := ⋯ }

Tactic:
rw [cfcHomSuperset_apply, Set.domRestrict_apply, cfc_apply _ _ x.2.1 (hf.mono x.2.2)]

Goal state after:
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : ContinuousStar A
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
x : ↑{a | p a ∧ spectrum 𝕜 a ⊆ s}
⊢ (cfcHom ⋯) { toFun := (spectrum 𝕜 ↑x).domRestrict f, continuous_toFun := ⋯ } =
    (cfcHom ⋯)
      ({ toFun := s.domRestrict f, continuous_toFun := ⋯ }.comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
have h₁ : 0 ≤ (x : ℝ) := NNReal.zero_le_coe
    rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x

Tactic:
have h_cpct : IsCompact (spectrum ℝ a) := isCompact_iff_compactSpace.mpr inferInstance

Goal state after:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : Nontrivial A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
h_cpct : IsCompact (spectrum ℝ a)
⊢ (∃ r > 0, (algebraMap ℝ A) r ≤ a) ↔ ∀ x ∈ spectrum ℝ a, 0 < x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
⊢ a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
refine le_algebraMap_of_spectrum_le fun r hr => ?_

Goal state after:
case pos
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
nontriv : Nontrivial A
r : ℝ
hr : r ∈ spectrum ℝ a
⊢ r ≤ ‖a‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : IsSelfAdjoint a
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a

Tactic:
rw [← ha.toReal_spectralRadius_eq_norm]

Goal state after:
A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : IsSelfAdjoint a
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
⊢ ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
have : {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}.EqOn (cfc f) (cfc (fun x : ℝ ↦ f x.toNNReal)) :=
    fun a ha ↦ cfc_nnreal_eq_real _ _ ha.1

Goal state after:
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
⊢ ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ spectrum ℝ≥0 a ⊆ s
⊢ IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s

Tactic:
← SpectrumRestricts

Goal state after:
A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
this : Set.EqOn (cfc f) (cfc fun x ↦ ↑(f x.toNNReal)) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}
hf : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (NNReal.toReal '' s)
a : A
ha : (IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal) ∧ spectrum ℝ≥0 a ⊆ s
⊢ IsSelfAdjoint a ∧ spectrum ℝ a ⊆ NNReal.toReal '' s
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: case left.refine_1
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ ⟪x.1, x.1⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: case left.refine_2
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ⟪x.1, x.1⟫_A ≤ ⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: case right.refine_1
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ 0 ≤ ⟪x.2, x.2⟫_A

Tactic:
aesop (add safe apply CStarModule.inner_self_nonneg)

Goal state after: