awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
φ : A →⋆ₙₐ[S] B
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (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:
NonUnitalStarAlgHomClass.map_cfcₙ φ f a

Premises used: NonUnitalStarAlgHomClass.map_cfcₙ
-- 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)
⊢ Continuous[inst_7, inst_11] (⇑ψ : (a : A) → B)

Tactic:
have : Continuous ψ := hφ
-- 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)
⊢ spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B) ⊆ spectrum R a

Tactic:
have h_spec := AlgHom.spectrum_apply_subset ψ a
-- 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
⊢ q ((ψ : (a : A) → B) a)

Tactic:
have hψa : q (ψ a) := hφa
-- 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_1 : 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 := ⋯ }
this :
  Eq (α := C((↑(spectrum R a) : Type u_2), R) →⋆ₐ[R] B) (ψ.comp (cfcHom (p := p) ha))
    (StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι))
⊢ ContinuousOn f (spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B))

Tactic:
have hf' : ContinuousOn f (spectrum R (ψ a)) := hf.mono h_spec
-- 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_1 : 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 := ⋯ }
this :
  Eq (α := C((↑(spectrum R a) : Type u_2), R) →⋆ₐ[R] B) (ψ.comp (cfcHom (p := p) ha))
    (StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι))
hf' : ContinuousOn f (spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B))
rw :
  Eq.{u_5 + 1} (α := B)
    ((φ : (a : A) → B)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
            { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
              C((↑(spectrum R a) : Type u_2), R) } :
          A) :
      B)
    ((cfcHom (p := q) hψa : (a : C((↑(spectrum R ((φ : (a : A) → B) a)) : Type u_2), R)) → B)
        { toFun := (spectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B)).restrict (π := fun (a : R) ↦ R) f,
          continuous_toFun := ⋯ : C((↑(spectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B)) : Type u_2), R) } :
      B)
⊢ (φ : (a : A) → B) (cfc (p := p) f a) = cfc (p := q) f ((φ : (a : A) → B) a)

Tactic:
rw [cfc_apply .., cfc_apply ..]

Premises used: cfc_apply
-- 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_1 : 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 := ⋯ }
this :
  Eq (α := C((↑(spectrum R a) : Type u_2), R) →⋆ₐ[R] B) (ψ.comp (cfcHom (p := p) ha))
    (StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι))
hf' : ContinuousOn f (spectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B))
⊢ Eq.{u_5 + 1} (α := B)
    ((φ : (a : A) → B)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_2), R)) → A)
            { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
              C((↑(spectrum R a) : Type u_2), R) } :
          A) :
      B)
    ((cfcHom (p := q) hψa : (a : C((↑(spectrum R ((φ : (a : A) → B) a)) : Type u_2), R)) → B)
        { toFun := (spectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B)).restrict (π := fun (a : R) ↦ R) f,
          continuous_toFun := ⋯ : C((↑(spectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B)) : Type u_2), R) } :
      B)

Tactic:
congrm($(this) ⟨_, hf.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 := ⋯ }
suffices :
  Eq (α := C((↑(spectrum R a) : Type u_2), R) →⋆ₐ[R] B) (ψ.comp (cfcHom (p := p) ha))
    (StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι))
⊢ (φ : (a : A) → B) (cfc (p := p) f a) = cfc (p := q) f ((φ : (a : A) → B) a)

Tactic:
suffices ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι) by
    have hf' : ContinuousOn f (spectrum R (ψ a)) := hf.mono h_spec
    rw [cfc_apply .., cfc_apply ..]
    congrm($(this) ⟨_, hf.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 := ⋯ }
⊢ Eq (α := C((↑(spectrum R a) : Type u_2), R) →⋆ₐ[R] B) (ψ.comp (cfcHom (p := p) ha))
    (StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι))

Tactic:
ContinuousMap.UniqueHom.eq_of_continuous_of_map_id _ _ _ ?_ ?_ ?apply_id

Premises used: ContinuousMap.UniqueHom.eq_of_continuous_of_map_id
-- 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] (⇑(ψ.comp (cfcHom (p := p) ha)) : (a : C((↑(spectrum R a) : Type u_2), R)) → B)
refine_2 :
  Continuous[_, inst_11]
    (⇑(StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι)) :
      (a : C((↑(spectrum R a) : Type u_2), R)) → B)
refine :
  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)
⊢ Eq (α := C((↑(spectrum R a) : Type u_2), R) →⋆ₐ[R] B) (ψ.comp (cfcHom (p := p) ha))
    (StarAlgHom.comp (cfcHom (p := q) hψa) (ContinuousMap.compStarAlgHom' R R ι))

Tactic:
refine ContinuousMap.UniqueHom.eq_of_continuous_of_map_id _ _ _ ?_ ?_ ?apply_id

Premises used: ContinuousMap.UniqueHom.eq_of_continuous_of_map_id
-- 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 := ⋯ }
trans :
  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)
    ((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)
trans₁ :
  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)
⊢ 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:
trans cfcHom hψa (.restrict (spectrum R (ψ a)) (.id R))

Premises used: spectrum, 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 := ⋯ }
⊢ 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)
    ((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)

Tactic:
simp [cfcHom_id]

Premises used: cfcHom_id