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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
suffices :
  Eq (α := C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) (ψ.comp (cfcₙHom (p := p) ha))
    (NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)

Tactic:
suffices ψ.comp (cfcₙHom ha) =
      (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) by
    have hf' : ContinuousOn f (quasispectrum R (ψ a)) := hf.mono h_spec
    rw [cfcₙ_apply .., cfcₙ_apply ..]
    exact DFunLike.congr_fun this _
-- 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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Eq (α := C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) (ψ.comp (cfcₙHom (p := p) ha))
    (NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))

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

Premises used: ContinuousMapZero.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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
refine_1 :
  Continuous[_, inst_16]
    (⇑(ψ.comp (cfcₙHom (p := p) ha) : C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) :
      (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
refine_2 :
  Continuous[_, inst_16]
    (⇑(NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι)) :
      (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
refine :
  Eq.{u_5 + 1} (α := B)
    (((ψ.comp (cfcₙHom (p := p) ha) : C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) :
          (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum R a)) :
      B)
    ((NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) :
          (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum R a)) :
      B)
⊢ Eq (α := C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) (ψ.comp (cfcₙHom (p := p) ha))
    (NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))

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

Premises used: ContinuousMapZero.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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Eq.{u_5 + 1} (α := B)
    (((ψ.comp (cfcₙHom (p := p) ha) : C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) :
          (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum R a)) :
      B)
    ((cfcₙHom (p := q) hψa : (a : C((↑(quasispectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) :
          C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), R)₀) :
      B)

Tactic:
simp [cfcₙHom_id]

Premises used: cfcₙHom_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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Eq.{u_5 + 1} (α := B)
    ((cfcₙHom (p := q) hψa : (a : C((↑(quasispectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) :
          C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), R)₀) :
      B)
    ((NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) :
          (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum R a)) :
      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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Eq.{u_5 + 1} (α := B)
    (((ψ.comp (cfcₙHom (p := p) ha) : C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) :
          (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum R a)) :
      B)
    ((NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) :
          (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)
        (ContinuousMapZero.id (quasispectrum R a)) :
      B)

Tactic:
case apply_id =>
    trans cfcₙHom hψa (.id (quasispectrum R (ψ a)))
    · simp [cfcₙHom_id]
    · congr

Premises used: cfcₙHom_id, quasispectrum, ContinuousMapZero.id, cfcₙHom, DFunLike.coe
-- 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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
refine_1 :
  Continuous[_, inst_16]
    (Function.comp.{u_2 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑ψ : (a : A) → B)
      (⇑(cfcₙHom (p := p) ha) : (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → A))
⊢ Continuous[_, inst_16]
    (⇑(ψ.comp (cfcₙHom (p := p) ha) : C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) :
      (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)

Tactic:
dsimp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]

Premises used: ContinuousMapZero.nonUnitalStarAlgHom_precomp
-- 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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous[_, inst_16]
    (Function.comp.{u_2 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑ψ : (a : A) → B)
      (⇑(cfcₙHom (p := p) ha) : (a : C((↑(quasispectrum 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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
refine_2 :
  Continuous[_, inst_16]
    (Function.comp (β := C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), R)₀)
      (⇑(cfcₙHom (p := q) hψa) : (a : C((↑(quasispectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)₀) → B)
      fun (g : C((↑(quasispectrum R a) : Type u_2), R)₀) ↦ g.comp ι)
⊢ Continuous[_, inst_16]
    (⇑(NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι)) :
      (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → B)

Tactic:
dsimp [ContinuousMapZero.nonUnitalStarAlgHom_precomp]

Premises used: ContinuousMapZero.nonUnitalStarAlgHom_precomp
-- 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 : 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
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
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 →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous[_, inst_16]
    (Function.comp (β := C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2), R)₀)
      (⇑(cfcₙHom (p := q) hψa) : (a : C((↑(quasispectrum R ((ψ : (a : A) → B) a)) : Type u_2), R)₀) → B)
      fun (g : C((↑(quasispectrum R a) : Type u_2), R)₀) ↦ g.comp ι)

Tactic:
fun_prop