awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
⊢ Continuous[_, inst_5]
    (⇑φ : (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)

Tactic:
cfcHom_continuous ha |>.comp f'.continuous_precomp

Premises used: cfcHom_continuous, Continuous.comp, ContinuousMap.continuous_precomp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
⊢ Continuous[_, inst_5]
    (⇑φ : (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)

Tactic:
exact cfcHom_continuous ha |>.comp f'.continuous_precomp

Premises used: cfcHom_continuous, Continuous.comp, ContinuousMap.continuous_precomp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
refine_2 :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (comp
          (restrict
            (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
            (ContinuousMap.id R))
          f') :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)
        (restrict
          (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
          (ContinuousMap.id R)) :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)

Tactic:
simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply]

Premises used: StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
refine_2 :
  comp
      (restrict
        (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
        (ContinuousMap.id R))
      f' =
    f
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (comp
          (restrict
            (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
            (ContinuousMap.id R))
          f') :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
refine_2 :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R)
      ((comp
              (restrict
                (spectrum.{u_1, u_2} R (A := A)
                  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
                (ContinuousMap.id R))
              f' :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          x :
        R)
      ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
⊢ comp
      (restrict
        (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
        (ContinuousMap.id R))
      f' =
    f

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
x : (↑(spectrum R a) : Type u_1)
⊢ Eq (α := R)
    ((comp
            (restrict
              (spectrum.{u_1, u_2} R (A := A)
                ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
              (ContinuousMap.id R))
            f' :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        x :
      R)
    ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)

Tactic:
simp [hff']
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
        (cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) }
      else 0 :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) }

Tactic:
rw [cfc_def, dif_pos ⟨ha, hf⟩]

Premises used: dif_pos, cfc_def
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a)
h :
  ∀ (i : ι),
    cfc (p := p) (f i) a =
      (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) }
⊢ Eq (α := (i : ι) → A) (fun (i : ι) ↦ cfc (p := p) (f i) a) fun (i : ι) ↦
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) }

Tactic:
ext i
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a)
i : ι
⊢ cfc (p := p) (f i) a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) }

Tactic:
simp only [cfc_apply (f i) a ha (hf i)]

Premises used: cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (spectrum R a))
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfc (p := p) f a = 0

Tactic:
rw [cfc_def, dif_neg ha]

Premises used: cfc_def, dif_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
ha : ¬p a
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfc (p := p) f a = 0

Tactic:
rw [cfc_def, dif_neg (not_and_of_not_left _ ha)]

Premises used: not_and_of_not_left, cfc_def, dif_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ¬ContinuousOn f (spectrum R a)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfc (p := p) f a = 0

Tactic:
rw [cfc_def, dif_neg (not_and_of_not_right _ hf)]

Premises used: cfc_def, dif_neg, not_and_of_not_right
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    (f : (a : (↑(spectrum R a) : Type u_1)) → R) x =
      (spectrum R a).restrict (π := fun (a : R) ↦ R)
        (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
          (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
        x
⊢ (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
x : (↑(spectrum R a) : Type u_1)
⊢ (f : (a : (↑(spectrum R a) : Type u_1)) → R) x =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
      x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)

Tactic:
have h : f = (spectrum R a).restrict (Function.extend Subtype.val f g) := by
    ext; simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h :
  (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
⊢ ContinuousOn
    (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
      (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
    (spectrum R a)

Tactic:
have hg : ContinuousOn (Function.extend Subtype.val f g) (spectrum R a) :=
    continuousOn_iff_continuous_restrict.mpr <| h ▸ map_continuous f
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h :
  (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
hg :
  ContinuousOn
    (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
      (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
    (spectrum R a)
rw :
  Eq.{u_2 + 1} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        {
          toFun :=
            (spectrum R a).restrict (π := fun (a : R) ↦ R)
              (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
                (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g),
          continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_1), R) } :
      A)
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f =
    cfc (p := p)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
      a

Tactic:
rw [cfc_apply ..]

Premises used: cfc_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h :
  (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
hg :
  ContinuousOn
    (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
      (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
    (spectrum R a)
⊢ Eq.{u_2 + 1} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        {
          toFun :=
            (spectrum R a).restrict (π := fun (a : R) ↦ R)
              (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
                (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g),
          continuous_toFun := ⋯ : C((↑(spectrum R a) : Type u_1), R) } :
      A)

Tactic:
congr!