awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ 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:
have : Isometry ((StarAlgebra.elemental ℂ a).subtype.comp <| continuousFunctionalCalculus a :
        C(spectrum ℂ a, ℂ) →⋆ₐ[ℂ] A) :=
      isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
⊢ ∃ (φ : 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)

Tactic:
⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩

Premises used: Isometry.injective, Isometry.continuous, And.intro, Exists.intro
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)) → ℂ)
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)
⊢ ∃ (φ : 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)

Tactic:
refine ⟨_, this.continuous, this.injective, ?hom_id, ?hom_map_spectrum, ?predicate_hom⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
⊢ (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:
congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a

Premises used: congr_arg, Subtype.val, continuousFunctionalCalculus_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
⊢ (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:
exact congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a

Premises used: congr_arg, Subtype.val, continuousFunctionalCalculus_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
⊢ (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:
case hom_id => exact congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a

Premises used: congr_arg, Subtype.val, continuousFunctionalCalculus_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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), ℂ)
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)) → ℂ)
⊢ 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:
simp only [StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype]

Premises used: StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)) → ℂ)
rw₂ rw₃ :
  Eq (α := Set ℂ) (Set.range (ι := (↑(spectrum ℂ a) : Type)) (⇑f : (a : (↑(spectrum ℂ a) : Type)) → ℂ))
    (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)) → ℂ)

Tactic:
rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
        AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]

Premises used: StarSubalgebra.spectrum_eq, continuousFunctionalCalculus, AlgEquiv.spectrum_eq, ContinuousMap.spectrum_eq_range
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)) → ℂ)

Tactic:
case hom_map_spectrum =>
      intro f
      simp only [StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype]
      rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
        AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]

Premises used: StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.spectrum_eq, StarSubalgebra.coe_subtype, continuousFunctionalCalculus, AlgEquiv.spectrum_eq, ContinuousMap.spectrum_eq_range
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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 :
  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)
⊢ 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)

Tactic:
rw [← map_star]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
    ((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:
Commute.all (star f) f |>.map _

Premises used: Commute.map, Commute.all, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
    ((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:
exact Commute.all (star f) f |>.map _

Premises used: Commute.map, Commute.all, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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), ℂ)),
    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:
exact fun f ↦ ⟨by rw [← map_star]; exact Commute.all (star f) f |>.map _⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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), ℂ)),
    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:
case predicate_hom => exact fun f ↦ ⟨by rw [← map_star]; exact Commute.all (star f) f |>.map _⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)))

Tactic:
cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_

Premises used: cfcHom_eq_of_continuous_of_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)
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
⊢ Eq (α := C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] A) (cfcHom (p := IsStarNormal) ha)
    (StarAlgHom.comp (StarSubalgebra.subtype (elemental ℂ a))
      (↑(continuousFunctionalCalculus a) : C((↑(spectrum ℂ a) : Type), ℂ) →⋆ₐ[ℂ] ↥(elemental ℂ a)))

Tactic:
refine cfcHom_eq_of_continuous_of_map_id ha _ ?_ ?_

Premises used: cfcHom_eq_of_continuous_of_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ 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:
continuous_subtype_val.comp <|
      (StarAlgEquiv.isometry (continuousFunctionalCalculus a)).continuous

Premises used: continuous_subtype_val, Continuous.comp, continuousFunctionalCalculus, Isometry.continuous, StarAlgEquiv.isometry
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ 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:
exact continuous_subtype_val.comp <|
      (StarAlgEquiv.isometry (continuousFunctionalCalculus a)).continuous

Premises used: continuous_subtype_val, Continuous.comp, continuousFunctionalCalculus, Isometry.continuous, StarAlgEquiv.isometry
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ (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:
simp [continuousFunctionalCalculus_map_id a]

Premises used: continuousFunctionalCalculus_map_id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
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)
⊢ Isometry (α := C((↑(spectrum ℂ a) : Type), ℂ)) (β := A)
    (⇑(cfcHom (p := IsStarNormal) ha) : (a : C((↑(spectrum ℂ a) : Type), ℂ)) → A)

Tactic:
rw [cfcHom_eq_of_isStarNormal]

Premises used: cfcHom_eq_of_isStarNormal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ 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:
isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)

Premises used: Isometry.comp, continuousFunctionalCalculus, isometry_subtype_coe, StarAlgEquiv.isometry
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
a : A
ha : IsStarNormal a
⊢ 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:
exact isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)

Premises used: Isometry.comp, continuousFunctionalCalculus, isometry_subtype_coe, StarAlgEquiv.isometry
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : CStarAlgebra A
⊢ IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint

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

Premises used: SpectrumRestricts.isometric_cfc, Complex.isometry_ofReal, IsSelfAdjoint.zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
⊢ NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℂ A IsStarNormal

Tactic:
RCLike.nonUnitalContinuousFunctionalCalculusIsClosedEmbedding Unitization.isStarNormal_inr

Premises used: RCLike.nonUnitalContinuousFunctionalCalculusIsClosedEmbedding, Unitization.isStarNormal_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
⊢ Eq (α := ContinuousMapZero (↑(σₙ ℂ a) : Type) ℂ →⋆ₙₐ[ℂ] Unitization ℂ A)
    (NonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom ℂ A) (cfcₙHom (p := IsStarNormal) ha))
    (cfcₙAux (p := IsStarNormal) (p₁ := IsStarNormal) ⋯ a ha)

Tactic:
inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux isStarNormal_inr a ha

Premises used: Set.Mem, inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux, Unitization.isStarNormal_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
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)

Tactic:
AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_

Premises used: AddMonoidHomClass.isometry_of_norm, Set.Mem, setOf
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
refine :
  ∀ (f : C((↑(σₙ ℂ a) : Type), ℂ)₀),
    norm (E := A) ((cfcₙHom (p := IsStarNormal) ha : (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → A) f : A) = ‖f‖
⊢ Isometry (α := C((↑(σₙ ℂ a) : Type), ℂ)₀) (β := A)
    (⇑(cfcₙHom (p := IsStarNormal) ha) : (a : C((↑(σₙ ℂ a) : Type), ℂ)₀) → A)

Tactic:
refine AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_

Premises used: AddMonoidHomClass.isometry_of_norm