awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
inst_22 : FunLike F A B
inst_23 : AlgHomClass F S A B
inst_24 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R (↑φ : A →⋆ₐ[S] B)
this : Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)
h_spec : spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), (↑(spectrum R a) : Type u_2)) :=
  { toFun := Set.inclusion (s := spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := spectrum R a) h_spec,
    continuous_toFun := ⋯ }
⊢ Eq.{u_5 + 1} (α := B)
    ((cfcHom (p := q) hψa : (a : C((↑(spectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)) → B)
        (ContinuousMap.restrict (spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (ContinuousMap.id R)) :
      B)
    ((StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι) :
          (a : C((↑(spectrum R a) : Type u_2), R)) → B)
        (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) :
      B)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
inst_22 : FunLike F A B
inst_23 : AlgHomClass F S A B
inst_24 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R (↑φ : A →⋆ₐ[S] B)
this : Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)
h_spec : spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), (↑(spectrum R a) : Type u_2)) :=
  { toFun := Set.inclusion (s := spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := spectrum R a) h_spec,
    continuous_toFun := ⋯ }
⊢ Eq.{u_5 + 1} (α := B)
    ((ψ.comp (cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_2), R)) → B)
        (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) :
      B)
    ((StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι) :
          (a : C((↑(spectrum R a) : Type u_2), R)) → B)
        (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) :
      B)

Tactic:
case apply_id =>
    trans cfcHom hψa (.restrict (spectrum R (ψ a)) (.id R))
    · simp [cfcHom_id]
    · congr

Premises used: spectrum, cfcHom_id, cfcHom, ContinuousMap.id, DFunLike.coe, ContinuousMap.restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
inst_22 : FunLike F A B
inst_23 : AlgHomClass F S A B
inst_24 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R (↑φ : A →⋆ₐ[S] B)
this : Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)
h_spec : spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), (↑(spectrum R a) : Type u_2)) :=
  { toFun := Set.inclusion (s := spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := spectrum R a) h_spec,
    continuous_toFun := ⋯ }
refine_1 :
  Continuous[_, inst_11]
    (Function.comp.{u_2 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑ψ : (a : A) → B)
      (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_2), R)) → A))
⊢ Continuous[_, inst_11] (⇑(ψ.comp (cfcHom (p := p) ha)) : (a : C((↑(spectrum R a) : Type u_2), R)) → B)

Tactic:
dsimp [ContinuousMap.compStarAlgHom']

Premises used: ContinuousMap.compStarAlgHom'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
inst_22 : FunLike F A B
inst_23 : AlgHomClass F S A B
inst_24 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R (↑φ : A →⋆ₐ[S] B)
this : Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)
h_spec : spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), (↑(spectrum R a) : Type u_2)) :=
  { toFun := Set.inclusion (s := spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := spectrum R a) h_spec,
    continuous_toFun := ⋯ }
⊢ Continuous[_, inst_11]
    (Function.comp.{u_2 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑ψ : (a : A) → B)
      (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_2), R)) → A))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
inst_22 : FunLike F A B
inst_23 : AlgHomClass F S A B
inst_24 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R (↑φ : A →⋆ₐ[S] B)
this : Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)
h_spec : spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), (↑(spectrum R a) : Type u_2)) :=
  { toFun := Set.inclusion (s := spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := spectrum R a) h_spec,
    continuous_toFun := ⋯ }
refine_2 :
  Continuous[_, inst_11]
    (Function.comp (β := C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), R))
      (⇑(cfcHom (p := q) hψa) : (a : C((↑(spectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)) → B)
      fun (g : C((↑(spectrum R a) : Type u_2), R)) ↦ g.comp ι)
⊢ Continuous[_, inst_11]
    (⇑(StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι)) :
      (a : C((↑(spectrum R a) : Type u_2), R)) → B)

Tactic:
dsimp [ContinuousMap.compStarAlgHom']

Premises used: ContinuousMap.compStarAlgHom'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
inst_22 : FunLike F A B
inst_23 : AlgHomClass F S A B
inst_24 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R (↑φ : A →⋆ₐ[S] B)
this : Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)
h_spec : spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), (↑(spectrum R a) : Type u_2)) :=
  { toFun := Set.inclusion (s := spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := spectrum R a) h_spec,
    continuous_toFun := ⋯ }
⊢ Continuous[_, inst_11]
    (Function.comp (β := C((↑(spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), R))
      (⇑(cfcHom (p := q) hψa) : (a : C((↑(spectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)) → B)
      fun (g : C((↑(spectrum R a) : Type u_2), R)) ↦ g.comp ι)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : Ring B
inst_10 : StarRing B
inst_11 : TopologicalSpace B
inst_12 : Algebra R B
inst_13 : CommSemiring S
inst_14 : Algebra R S
inst_15 : Algebra S A
inst_16 : Algebra S B
inst_17 : IsScalarTower R S A
inst_18 : IsScalarTower R S B
inst_19 : ContinuousFunctionalCalculus R A p
inst_20 : ContinuousFunctionalCalculus R B q
inst_21 : ContinuousMap.UniqueHom R B
φ : A →⋆ₐ[S] B
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hφ : Continuous[inst_7, inst_11] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
⊢ (φ : (a : A) → B) (cfc (p := p) f a) = cfc (p := q) f ((φ : (a : A) → B) a)

Tactic:
StarAlgHomClass.map_cfc φ f a

Premises used: StarAlgHomClass.map_cfc
-- 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
⊢ IsCompact (spectrum R a)

Tactic:
isCompact_iff_compactSpace.mpr inferInstance

Premises used: Iff.mpr, isCompact_iff_compactSpace, inferInstance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Goal:
R : Type u_1
A : Type u_2
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
inst_9 : UniqueHom R A
a : A
inst_10 : CompactSpace.{u_1} (↑(spectrum R a) : Type u_1)
φ ψ : C((↑(spectrum R a) : Type u_1), R) →⋆ₐ[R] A
hφ : Continuous[_, inst_5] (⇑φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
hψ : Continuous[_, inst_5] (⇑ψ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (restrict (spectrum R a) (ContinuousMap.id R)) : A)
    ((ψ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (restrict (spectrum R a) (ContinuousMap.id R)) : A)
⊢ φ = ψ

Tactic:
UniqueHom.eq_of_continuous_of_map_id (spectrum R a) φ ψ hφ hψ h

Premises used: spectrum, ContinuousMap.UniqueHom.eq_of_continuous_of_map_id
-- 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
⊢ Continuous[_, inst_5] (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
(ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.1

Premises used: Exists.choose_spec, ContinuousFunctionalCalculus.exists_cfc_of_predicate, And.left
-- 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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := C((↑(spectrum R a) : Type u_1), R)) (β := A)
    (⇑(cfcHom (p := p) ha) : (a : C((↑(spectrum R a) : Type u_1), R)) → A)

Tactic:
(ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.1

Premises used: Exists.choose_spec, ContinuousFunctionalCalculus.exists_cfc_of_predicate, And.right, And.left
-- 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
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (restrict (spectrum R a) (ContinuousMap.id R)) = a

Tactic:
(ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.1

Premises used: Exists.choose_spec, ContinuousFunctionalCalculus.exists_cfc_of_predicate, And.right, And.left
-- 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
f : C((↑(spectrum R a) : Type u_1), R)
⊢ spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A) =
    Set.range (ι := (↑(spectrum R a) : Type u_1)) (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R)

Tactic:
(ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.2.1 f

Premises used: Exists.choose_spec, ContinuousFunctionalCalculus.exists_cfc_of_predicate, And.right, And.left
-- 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
f : C((↑(spectrum R a) : Type u_1), R)
⊢ p ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)

Tactic:
(ContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.2.2 f

Premises used: Exists.choose_spec, ContinuousFunctionalCalculus.exists_cfc_of_predicate, And.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
ha : p a
inst_9 : UniqueHom R A
φ : C((↑(spectrum R a) : Type u_1), R) →⋆ₐ[R] A
hφ₁ : Continuous[_, inst_5] (⇑φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
hφ₂ : (φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (restrict (spectrum R a) (ContinuousMap.id R)) = a
rw : a = (φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (restrict (spectrum R a) (ContinuousMap.id R))
rw₁ rw₂ : a = a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (restrict (spectrum R a) (ContinuousMap.id R)) :
      A)
    ((φ : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (restrict (spectrum R a) (ContinuousMap.id R)) : A)

Tactic:
rw [cfcHom_id ha, hφ₂]

Premises used: cfcHom_id
-- 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')
suffices : cfcHom (p := p) ⋯ = φ
⊢ Eq.{u_2 + 1} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) (g.comp f') : A)
    ((cfcHom (p := p) ⋯ :
          (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)
        g :
      A)

Tactic:
suffices cfcHom (cfcHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
-- 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')
⊢ cfcHom (p := p) ⋯ = φ

Tactic:
cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_

Premises used: cfcHom_eq_of_continuous_of_map_id, cfcHom_predicate
-- 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_1 :
  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)
refine_2 :
  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)
⊢ cfcHom (p := p) ⋯ = φ

Tactic:
refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_

Premises used: cfcHom_eq_of_continuous_of_map_id, cfcHom_predicate