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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ ‖ψ s‖₊ ≤ ‖s‖₊

Tactic:
suffices this : spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s by
      rwa [(hs.map ψ).spectralRadius_eq_nnnorm, hs.spectralRadius_eq_nnnorm, coe_le_coe]
        at this

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
a : A
ψ : Unitization ℂ A →⋆ₐ[ℂ] Unitization ℂ B
x s : Unitization ℂ A
hs : IsSelfAdjoint s
⊢ spectralRadius ℂ (ψ s) ≤ spectralRadius ℂ s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → Compacts β
g : α → β → γ
hf : Continuous[inst✝², _] f
hg : Continuous[instTopologicalSpaceProd, inst✝] (Function.uncurry g)
x : α
| Compacts.map (g x) ⋯ (f x)

Tactic:
equals ({x} ×ˢ f x).map g.uncurry hg => ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
⊢ ∀ (a : Compacts α), IsOpen {a}

Tactic:
intro K

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : DiscreteTopology α
K : Compacts α
⊢ IsOpen {K}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case refine_1
α : 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
⊢ {K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty} ∈ 𝓝 K

Tactic:
filter_upwards [
      (isOpen_subsets_of_isOpen isOpen_interior).mem_nhds hLK,
      (Filter.eventually_all_finite hu₁).mpr fun U hU =>
        (isOpen_inter_nonempty_of_isOpen isOpen_interior).mem_nhds (hMK U hU)] with K' h₁ h₂
    exact ⟨h₁.trans interior_subset,
      fun U hU => (h₂ U hU).mono (inter_subset_inter_right _ interior_subset)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
f : α → β
inst✝ : SeparableSpace α
⊢ SeparableSpace (Compacts α)

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := exists_countable_dense α
  refine ⟨_, (countable_ofPred_finite_subset hs₁).preimage SetLike.coe_injective, ?_⟩
  simp [dense_iff_closure_eq, closure_finite_subsets, hs₂.closure_eq]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakDual

Goal state before:
pp: case mpr
ι : Type u_4
𝕜 : Type u_5
E : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E →ₗ[𝕜] 𝕜
φ : E →ₗ[𝕜] 𝕜
t𝕜 : TopologicalSpace 𝕜 := inferInstance
t : TopologicalSpace E := ⨅ i, induced (⇑(f i)) t𝕜
this✝ : IsTopologicalAddGroup E
this : WithSeminorms fun i ↦ (f i).toSeminorm
H : ∃ s c, φ.toSeminorm ≤ c • s.sup fun i ↦ (f i).toSeminorm
⊢ Continuous[⨅ i, induced (⇑(f i)) inferInstance, inferInstance] ⇑φ

Tactic:
· exact WithSeminorms.continuous_normedSpace_rng _ this _ H

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

Goal state before:
pp: case neg
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)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
this : ‖(1 - (↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ 1
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ ≤ ε / 2

Tactic:
calc
        ‖f x - f x * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g x‖₊ =
            ‖f x * (1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ := by
          simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]
        _ ≤ ε / 2 * ‖(1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
          ((nnnorm_mul_le _ _).trans
            (mul_le_mul_left (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
        _ ≤ ε / 2 := by simpa only [mul_one] using! mul_le_mul_right this _

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ 1 = f x

Tactic:
apply (hft _).symm

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : LocallyCompactSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝²] t
hd : Disjoint s t
k : Set X
k_comp : IsCompact k
k_closed : IsClosed[inst✝²] k
sk : s ⊆ interior k
kt : k ⊆ tᶜ
f : X → ℝ
hf : Continuous[inst✝², _] f
hfs : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 0 s
hft : EqOn (⇑{ toFun := f, continuous_toFun := hf }) 1 (interior k)ᶜ
h'f : ∀ (x : X), { toFun := f, continuous_toFun := hf } x ∈ Icc 0 1
A : t ⊆ (interior k)ᶜ
x : X
hx : x ∉ k
⊢ x ∈ (interior k)ᶜ
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsSelfAdjoint (f i)) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
h : ∀ i ∈ insert j s, IsSelfAdjoint (f i)
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
simp_all [(h j (by simp)).nnnorm_add_eq_max (by cfc_tac) this]

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

Goal state before:
pp: 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
a : A
ha : ¬IsSelfAdjoint a
h : IsSelfAdjoint (-a)
⊢ IsSelfAdjoint a

Tactic:
simpa using h.neg

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

Goal state before:
pp: 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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
⊢ a⁺ = b → a⁻ = c

Tactic:
rintro rfl
    exact negPart_eq_of_eq_PosPart_sub habc hc

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

Goal state before:
pp: case star_id
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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) (star (ContinuousMapZero.id s)) * (cfcₙHomSuperset hc' hcs) g = 0

Tactic:
rw [star_trivial]

Goal state after:
case star_id
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✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b c : A
habc : a = b - c
hbc : b * c = 0
hb : 0 ≤ b
hc : 0 ≤ c
hb' : IsSelfAdjoint b
hc' : IsSelfAdjoint (-c)
ha : IsSelfAdjoint a
s : Set ℝ := σₙ ℝ a ∪ σₙ ℝ b ∪ σₙ ℝ (-c)
hs : CompactSpace ↑s
has : σₙ ℝ a ⊆ s
hbs : σₙ ℝ b ⊆ s
hcs : σₙ ℝ (-c) ⊆ s
this : Fact (0 ∈ s)
f g : C(↑s, ℝ)₀
⊢ (cfcₙHomSuperset hb' hbs) (ContinuousMapZero.id s) * (cfcₙHomSuperset hc' hcs) g = 0
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Bornology.IsBounded Set.univ

Tactic:
rw [Metric.isBounded_iff_ediam_ne_top, ← lt_top_iff_ne_top]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace γ
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
⊢ Metric.ediam Set.univ < ∞
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfcₙ (fun x ↦ x⁺) ((algebraMap ℝ≥0 A) r) = (algebraMap ℝ≥0 A) r

Tactic:
cfcₙ_eq_cfc,

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfc (fun x ↦ x⁺) ((algebraMap ℝ≥0 A) r) = (algebraMap ℝ≥0 A) r
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : StarRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
ha : 0 ≤ a
⊢ sqrt a * sqrt a = a

Tactic:
rw [← nnrpow_two _, nnrpow_sqrt_two _]

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ f x - g x) a = cfc f a - cfc g a

Tactic:
cfc_nnreal_eq_real ..,

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) a = cfc f a - cfc g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) a = cfc f a - cfc g a

Tactic:
cfc_nnreal_eq_real ..,

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) a = cfc (fun x ↦ ↑(f x.toNNReal)) a - cfc g a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) a = cfc (fun x ↦ ↑(f x.toNNReal)) a - cfc g a

Tactic:
cfc_nnreal_eq_real ..,

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) a = cfc (fun x ↦ ↑(f x.toNNReal)) a - cfc (fun x ↦ ↑(g x.toNNReal)) a
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✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
hf' : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x ↦ ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Tactic:
cfc_nnreal_eq_real ..,

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✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
hf' : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x ↦ ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal)) a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x
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✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
hf' : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x ↦ ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal)) a ≤ cfc g a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x

Tactic:
cfc_nnreal_eq_real ..,

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✝³ : IsTopologicalRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f g : ℝ≥0 → ℝ≥0
a : A
ha_spec : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha : 0 ≤ a
hf' : ContinuousOn (fun x ↦ ↑(f x.toNNReal)) (spectrum ℝ a)
hg' : ContinuousOn (fun x ↦ ↑(g x.toNNReal)) (spectrum ℝ a)
⊢ cfc (fun x ↦ ↑(f x.toNNReal)) a ≤ cfc (fun x ↦ ↑(g x.toNNReal)) a ↔ ∀ x ∈ spectrum ℝ≥0 a, f x ≤ g x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = sqrt ↑b * ↑b ^ (-(1 / 2)) * a * (↑b ^ (-(1 / 2)) * sqrt ↑b)

Tactic:
simp only [CFC.sqrt_eq_rpow .., ← CFC.rpow_add b.isUnit]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
b : Aˣ
hb : IsStrictlyPositive ↑b
hbab : 0 ≤ ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2))
h : ↑b ^ (-(1 / 2)) * a * ↑b ^ (-(1 / 2)) ≤ 1
⊢ a = ↑b ^ (1 / 2 + -(1 / 2)) * a * ↑b ^ (-(1 / 2) + 1 / 2)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist (cfcₙ ((toFun {quasispectrum R a}) f) a) (cfcₙ ((toFun {quasispectrum R a}) g) a) ≤ ↑1 * edist f g

Tactic:
cfcₙ_apply ..,

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      ((cfcₙHom ha)
        { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) f), continuous_toFun := ⋯,
          map_zero' := hf0 })
      (cfcₙ ((toFun {quasispectrum R a}) g) a) ≤
    ↑1 * edist f g
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      ((cfcₙHom ha)
        { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) f), continuous_toFun := ⋯,
          map_zero' := hf0 })
      (cfcₙ ((toFun {quasispectrum R a}) g) a) ≤
    ↑1 * edist f g

Tactic:
cfcₙ_apply ..,

Goal state after:
case pos
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : MetricSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus R A p
a : A
ha : p a
f : R →ᵤ[{quasispectrum R a}] R
hf : ContinuousOn ((toFun {quasispectrum R a}) f) (quasispectrum R a)
hf0 : f 0 = 0
g : R →ᵤ[{quasispectrum R a}] R
hg : ContinuousOn ((toFun {quasispectrum R a}) g) (quasispectrum R a)
hg0 : g 0 = 0
⊢ edist
      ((cfcₙHom ha)
        { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) f), continuous_toFun := ⋯,
          map_zero' := hf0 })
      ((cfcₙHom ha)
        { toFun := (quasispectrum R a).domRestrict ((toFun {quasispectrum R a}) g), continuous_toFun := ⋯,
          map_zero' := hg0 }) ≤
    ↑1 * edist f g
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
this : ∑ i, c i • ↑(x i) ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
⊢ Tendsto (fun x_1 ↦ x_1 * ∑ i, c i • ↑(x i)) l (𝓝 (∑ i, c i • ↑(x i)))

Tactic:
Finset.mul_sum

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
n : ℕ
c : Fin n → ℂ
x : Fin n → ↑({x | 0 ≤ x} ∩ ball 0 1)
this : ∑ i, c i • ↑(x i) ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)
⊢ Tendsto (fun x_1 ↦ ∑ i, x_1 * c i • ↑(x i)) l (𝓝 (∑ i, c i • ↑(x i)))