awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
refine :
  (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
        (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
      (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
    a
⊢ ∃ (φ : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A),
    Continuous (X := C((↑(spectrum ℂ a) : Type), ℂ)) (Y := A) (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
      Function.Injective (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
          (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
        (φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              spectrum ℂ (A := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A) =
                Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)) ∧
            ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              IsStarNormal (R := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A)
have refine₁ : ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
  spectrum ℂ (A := A)
      ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
              (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
            (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
          f :
        A) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
Tactic: refine ⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
refine :
  (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
        (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
      (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
    a
refine₁ :
  ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
    spectrum ℂ (A := A)
        ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
                (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
              (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
            f :
          A) =
      Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
⊢ ∃ (φ : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A),
    Continuous (X := C((↑(spectrum ℂ a) : Type), ℂ)) (Y := A) (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
      Function.Injective (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
          (⇑φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) ∧
        (φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
            a ∧
          (∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              spectrum ℂ (A := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A) =
                Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)) ∧
            ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
              IsStarNormal (R := A) ((φ : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A) f : A)
have refine₂ : ∀ (f : C((↑(spectrum ℂ a) : Type), ℂ)),
  IsStarNormal (R := A)
    ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
            (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
          (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
        f :
      A)
Tactic: refine ⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
f : C((↑(spectrum ℂ a) : Type), ℂ)
⊢ spectrum ℂ (A := A)
      ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
              (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
            (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
          f :
        A) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
have simp : spectrum.{0, u_1} ℂ (A := A)
    (↑((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f) : A) =
  Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
Tactic: simp only [StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
f : C((↑(spectrum ℂ a) : Type), ℂ)
⊢ spectrum.{0, u_1} ℂ (A := A)
      (↑((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f) : A) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
have rw : spectrum ℂ (A := ↥(elemental ℂ a))
    ((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f :
      ↥(elemental ℂ a)) =
  Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
Tactic: rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
        AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
f : C((↑(spectrum ℂ a) : Type), ℂ)
rw :
  spectrum ℂ (A := ↥(elemental ℂ a))
      ((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f :
        ↥(elemental ℂ a)) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
⊢ spectrum.{0, u_1} ℂ (A := A)
      (↑((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f) : A) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
have rw₁ : spectrum ℂ f = Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
Tactic: rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
        AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
f : C((↑(spectrum ℂ a) : Type), ℂ)
rw :
  spectrum ℂ (A := ↥(elemental ℂ a))
      ((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f :
        ↥(elemental ℂ a)) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
rw₁ : spectrum ℂ f = Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
⊢ spectrum.{0, u_1} ℂ (A := A)
      (↑((continuousFunctionalCalculus a : (a_1 : C((↑(spectrum ℂ a) : Type), ℂ)) → ↥(elemental ℂ a)) f) : A) =
    Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ)
have rw₂ : Eq (α := Set ℂ) (Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ))
  (Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ))
Tactic: rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
        AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
this :
  Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
f : C((↑(spectrum ℂ a) : Type), ℂ)
⊢ Commute (S := A)
    (star
        ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
              (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
            (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
          f) :
      A)
    ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
            (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
          (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
        f :
      A)
have rw : Commute (S := A)
  ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
        (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
      (star f) :
    A)
  ((StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
        (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
      f :
    A)
Tactic: rw [← map_star]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Eq (α := C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A) (cfcHom (p := IsStarNormal) ha)
    (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
      (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)))
have refine_1 : Continuous (X := C((↑(spectrum ℂ a) : Type), ℂ)) (Y := A)
  (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
        (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
    (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
Tactic: refine cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
refine_1 :
  Continuous (X := C((↑(spectrum ℂ a) : Type), ℂ)) (Y := A)
    (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
          (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
⊢ Eq (α := C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A) (cfcHom (p := IsStarNormal) ha)
    (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
      (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)))
have refine_2 : (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
        (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)) :
      (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
    (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) =
  a
Tactic: refine cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(cfcHom (p := IsStarNormal) ha) : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
have rw : Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
  (⇑(StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
        (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a))) :
    (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)
Tactic: rw [cfcHom_eq_of_isStarNormal]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Isometry (α := C((↑(σₙ ℂ a) : Type), ℂ)₀) (β := A)
    (⇑(cfcₙHom (p := IsStarNormal) ha) : (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → A)
have refine : ∀ (f : C((↑(σₙ ℂ a) : Type), ℂ)₀),
  norm (E := A) ((cfcₙHom (p := IsStarNormal) ha : (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → A) f : A) = ‖f‖
Tactic: refine AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
⊢ norm (E := A) ((cfcₙHom (p := IsStarNormal) ha : (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → A) f : A) = ‖f‖
have rw : norm (E := Unitization ℂ A)
    ((NonUnitalStarAlgHom.comp
            (NonUnitalStarAlgHom.comp
              (↑(cfcHom (p := IsStarNormal) sorry) :
                C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ) →⋆ₙₐ[ℂ] Unitization ℂ A)
              (↑(Homeomorph.compStarAlgEquiv' ℂ ℂ
                      (Homeomorph.setCongr (s := spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) (t := σₙ ℂ a)
                        sorry) :
                    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: rw [← norm_inr (𝕜 := ℂ), ← inrNonUnitalStarAlgHom_apply, ← NonUnitalStarAlgHom.comp_apply,
      inr_comp_cfcₙHom_eq_cfcₙAux a, cfcₙAux]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
⊢ 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‖
have simp : norm (E := Unitization ℂ A)
    ((cfcHom (p := IsStarNormal) sorry : (a : C((↑(spectrum ℂ (↑a : Unitization ℂ A)) : Type), ℂ)) → Unitization ℂ A)
        (((Homeomorph.compStarAlgEquiv' ℂ ℂ
                  (Homeomorph.setCongr (s := spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A)) (t := σₙ ℂ a)
                    sorry) :
                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: simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply,
      toContinuousMapHom_apply, NonUnitalStarAlgHom.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C((↑(σₙ ℂ a) : Type), ℂ)₀
⊢ 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‖
have rw : norm (E := C((↑(σₙ ℂ a) : Type), ℂ)) (↑f : C((↑(σₙ ℂ a) : Type), ℂ)) = ‖f‖
Tactic: rw [norm_cfcHom (a : Unitization ℂ A), StarAlgEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (hypothesis)
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
t : ℝ≥0
ha : IsSelfAdjoint a
ht : ‖a‖₊ ≤ t
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t
have 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∞)
Tactic: rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢
Cleared hypotheses: ht, this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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∞)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t
have 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 : ℂ) → ℝ)
Tactic: rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢
Cleared hypotheses: ht, this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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 : ℂ) → ℝ)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t
have 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 : ℂ) → ℝ)
Tactic: rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢
Cleared hypotheses: ht, this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (goal)
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 : ℂ) → ℝ)
⊢ SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0) ↔
    ‖HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (↑t : ℝ) : A) a‖₊ ≤ t
have 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)
Tactic: rw [← ENNReal.coe_le_coe, ← IsSelfAdjoint.spectralRadius_eq_nnnorm,
    ← SpectrumRestricts.spectralRadius_eq (f := Complex.reCLM)] at ht ⊢
Cleared hypotheses: ht, this