awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
rw :
  norm (E := Unitization ℂ A)
      ((NonUnitalStarAlgHom.comp
              (NonUnitalStarAlgHom.comp
                (↑(cfcHom (p := IsStarNormal) ⋯) :
                  C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ) →⋆ₙₐ[ℂ] Unitization ℂ A)
                (↑(Homeomorph.compStarAlgEquiv' ℂ ℂ
                        (Homeomorph.setCongr (s := spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) (t :=
                          σₙ ℂ a) ⋯) :
                      C((↑(σₙ ℂ a) : Type), ℂ) ≃⋆ₐ[ℂ]
                        C((↑(spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) : Type), ℂ)) :
                  C((↑(σₙ ℂ a) : Type), ℂ) →⋆ₙₐ[ℂ] C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ)))
              toContinuousMapHom :
            (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → Unitization ℂ A)
          f :
        Unitization ℂ A) =
    ‖f‖
⊢ norm (E := A) ((cfcₙHom (p := IsStarNormal) ha : (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → A) f : A) = ‖f‖

Tactic:
rw [← norm_inr (𝕜 := ℂ), ← inrNonUnitalStarAlgHom_apply, ← NonUnitalStarAlgHom.comp_apply,
      inr_comp_cfcₙHom_eq_cfcₙAux a, cfcₙAux]

Premises used: cfcₙAux, NonUnitalStarAlgHom.comp_apply, Unitization.inrNonUnitalStarAlgHom_apply, inr_comp_cfcₙHom_eq_cfcₙAux, Unitization.norm_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
simp :
  norm (E := Unitization ℂ A)
      ((cfcHom (p := IsStarNormal) ⋯ : (a : C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ)) → Unitization ℂ A)
          (((Homeomorph.compStarAlgEquiv' ℂ ℂ
                    (Homeomorph.setCongr (s := spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) (t := σₙ ℂ a)
                      ⋯) :
                  C((↑(σₙ ℂ a) : Type), ℂ) ≃⋆ₐ[ℂ]
                    C((↑(spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) : Type), ℂ)) :
                (a_1 : C((↑(σₙ ℂ a) : Type), ℂ)) → C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ))
              (↑f : C((↑(σₙ ℂ a) : Type), ℂ)) :
            C((↑(spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) : Type), ℂ)) :
        Unitization ℂ A) =
    ‖f‖
⊢ norm (E := Unitization ℂ A)
      ((NonUnitalStarAlgHom.comp
              (NonUnitalStarAlgHom.comp
                (↑(cfcHom (p := IsStarNormal) ⋯) :
                  C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ) →⋆ₙₐ[ℂ] Unitization ℂ A)
                (↑(Homeomorph.compStarAlgEquiv' ℂ ℂ
                        (Homeomorph.setCongr (s := spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) (t :=
                          σₙ ℂ a) ⋯) :
                      C((↑(σₙ ℂ a) : Type), ℂ) ≃⋆ₐ[ℂ]
                        C((↑(spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) : Type), ℂ)) :
                  C((↑(σₙ ℂ a) : Type), ℂ) →⋆ₙₐ[ℂ] C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ)))
              toContinuousMapHom :
            (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → Unitization ℂ A)
          f :
        Unitization ℂ A) =
    ‖f‖

Tactic:
simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
      toContinuousMapHom_apply, NonUnitalStarAlgHom.coe_coe]

Premises used: NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe, ContinuousMapZero.toContinuousMapHom_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
rw : norm (E := C((↑(σₙ ℂ a) : Type), ℂ)) (↑f : C((↑(σₙ ℂ a) : Type), ℂ)) = ‖f‖
⊢ norm (E := Unitization ℂ A)
      ((cfcHom (p := IsStarNormal) ⋯ : (a : C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ)) → Unitization ℂ A)
          (((Homeomorph.compStarAlgEquiv' ℂ ℂ
                    (Homeomorph.setCongr (s := spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) (t := σₙ ℂ a)
                      ⋯) :
                  C((↑(σₙ ℂ a) : Type), ℂ) ≃⋆ₐ[ℂ]
                    C((↑(spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) : Type), ℂ)) :
                (a_1 : C((↑(σₙ ℂ a) : Type), ℂ)) → C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ))
              (↑f : C((↑(σₙ ℂ a) : Type), ℂ)) :
            C((↑(spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) : Type), ℂ)) :
        Unitization ℂ A) =
    ‖f‖

Tactic:
rw [norm_cfcHom (a : Unitization ℂ A), StarAlgEquiv.norm_map]

Premises used: StarAlgEquiv.norm_map, Unitization.inr, norm_cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
⊢ norm (E := C((↑(σₙ ℂ a) : Type), ℂ)) (↑f : C((↑(σₙ ℂ a) : Type), ℂ)) = ‖f‖

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
⊢ NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint

Tactic:
QuasispectrumRestricts.isometric_cfc Complex.reCLM Complex.isometry_ofReal (.zero _)
    fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts

Premises used: Complex.isometry_ofReal, IsSelfAdjoint.zero, QuasispectrumRestricts.isometric_cfc
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
⊢ IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)

Tactic:
have : IsSelfAdjoint (algebraMap ℝ A t - a) := IsSelfAdjoint.algebraMap A (.all (t : ℝ)) |>.sub ha
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
rw :
  ∀ (ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
      spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)
rw₁ :
  ∀ (ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    SpectrumRestricts (R := ℝ) (S := ℂ) (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
      (⇑Complex.reCLM : (a : ℂ) → ℝ)
rw₂ :
  ∀ (ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)
rw₃ :
  ∀ (ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)),
    IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
rw₄ :
  ∀ (ht : (↑‖a‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞))
    (this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)), IsSelfAdjoint a
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t

Tactic:
rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢

Premises used: ENNReal.coe_le_coe, SpectrumRestricts.spectralRadius_eq, IsSelfAdjoint.spectralRadius_eq_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)

Tactic:
SpectrumRestricts.nnreal_iff_spectralRadius_le ht

Premises used: SpectrumRestricts.nnreal_iff_spectralRadius_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    spectralRadius ℝ (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a) ≤ (↑t : ℝ≥0∞)

Tactic:
exact SpectrumRestricts.nnreal_iff_spectralRadius_le ht

Premises used: SpectrumRestricts.nnreal_iff_spectralRadius_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this ha₁ : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
    (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Premises used: IsSelfAdjoint.spectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this ha₁ : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
    (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
try apply IsSelfAdjoint.spectrumRestricts

Premises used: IsSelfAdjoint.spectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℝ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
ha₁ : IsSelfAdjoint a
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
apply IsSelfAdjoint.spectrumRestricts

Premises used: IsSelfAdjoint.spectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
ha₁ : IsSelfAdjoint a
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ)

Tactic:
try apply IsSelfAdjoint.spectrumRestricts

Premises used: IsSelfAdjoint.spectrumRestricts
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ IsSelfAdjoint a

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : spectralRadius ℂ a ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : (↑‖a‖₊ : ℝ≥0∞) ≤ (↑t : ℝ≥0∞)
this : IsSelfAdjoint (HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a)
⊢ IsSelfAdjoint a

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
rw :
  ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a +
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (a + b) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [SpectrumRestricts.nnreal_iff_nnnorm (ha₁.add hb₁) (nnnorm_add_le a b), NNReal.coe_add,
    map_add, add_sub_add_comm]

Premises used: NNReal.coe_add, map_add, IsSelfAdjoint.add, add_sub_add_comm, nnnorm_add_le, SpectrumRestricts.nnreal_iff_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a +
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊

Tactic:
nnnorm_add_le _ _ |>.trans ?_

Premises used: LE.le.trans, nnnorm_add_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
refine :
  ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ +
      ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a +
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊

Tactic:
refine nnnorm_add_le _ _ |>.trans ?_

Premises used: LE.le.trans, nnnorm_add_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₁ : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ ≤ ‖a‖₊
h₂ : ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤ ‖b‖₊
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ +
      ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤
    ‖a‖₊ + ‖b‖₊

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₂ : IsSelfAdjoint a
h₃ : ‖a‖₊ ≤ ‖a‖₊
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖a‖₊ : ℝ) : A) a‖₊ ≤ ‖a‖₊

Tactic:
rw [← SpectrumRestricts.nnreal_iff_nnnorm]

Premises used: SpectrumRestricts.nnreal_iff_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
first | rfl | assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint a

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint a

Tactic:
first | rfl | assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖a‖₊ ≤ ‖a‖₊

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖a‖₊ ≤ ‖a‖₊

Tactic:
first | rfl | assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ h₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
h₃ : IsSelfAdjoint b
h₄ : ‖b‖₊ ≤ ‖b‖₊
⊢ ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑‖b‖₊ : ℝ) : A) b‖₊ ≤ ‖b‖₊

Tactic:
rw [← SpectrumRestricts.nnreal_iff_nnnorm]

Premises used: SpectrumRestricts.nnreal_iff_nnnorm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
first | rfl | assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint b

Tactic:
assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ IsSelfAdjoint b

Tactic:
first | rfl | assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖b‖₊ ≤ ‖b‖₊

Tactic:
rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
hb₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) b (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ‖b‖₊ ≤ ‖b‖₊

Tactic:
first | rfl | assumption
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
rw : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (id x) 2) '' spectrum ℝ a) x → 0 ≤ x
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) (HPow.hPow (β := ℕ) a 2) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)

Tactic:
rw [SpectrumRestricts.nnreal_iff, ← cfc_id (R := ℝ) a, ← cfc_pow .., cfc_map_spectrum ..]

Premises used: cfc_pow, Real, SpectrumRestricts.nnreal_iff, cfc_map_spectrum, cfc_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
x : ℝ
⊢ LE.le (α := ℝ) 0 ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (id x) 2) x)

Tactic:
sq_nonneg x

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
x : ℝ
⊢ LE.le (α := ℝ) 0 ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (id x) 2) x)

Tactic:
exact sq_nonneg x

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (-a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂

Premises used: SpectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
ha₂ : SpectrumRestricts (R := ℝ≥0) (S := ℝ) (-a) (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
ha₃ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ ∀ x ∈ spectrum ℝ (-a), 0 ≤ x

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂

Premises used: SpectrumRestricts.nnreal_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
apply : spectrum ℝ a ⊆ {0}
⊢ a = 0

Tactic:
apply CFC.eq_zero_of_spectrum_subset_zero (R := ℝ) a

Premises used: CFC.eq_zero_of_spectrum_subset_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
⊢ ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x

Tactic:
simp only [← spectrum.neg_eq, Set.mem_neg] at ha₂

Premises used: Set.mem_neg, spectrum.neg_eq