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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
n : ℕ
r : R
h :
  cfc (p := p)
      (fun (x : R) ↦
        Polynomial.eval (f x)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
      a =
    (aeval (cfc (p := p) f a) : (a : R[X]) → A)
      (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
monomial :
  cfc (p := p) (fun (x : R) ↦ r * f x ^ (n + 1)) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a ^ (n + 1))
⊢ cfc (p := p)
      (fun (x : R) ↦
        Polynomial.eval (f x)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))))
      a =
    (aeval (cfc (p := p) f a) : (a : R[X]) → A)
      (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
simp only [eval_mul, eval_C, eval_X_pow, map_mul, aeval_C, map_pow, aeval_X]

Premises used: Polynomial.eval_C, Polynomial.eval_X_pow, Polynomial.eval_mul, map_pow, map_mul, Polynomial.aeval_C, Polynomial.aeval_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
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
n : ℕ
r : R
h :
  cfc (p := p)
      (fun (x : R) ↦
        Polynomial.eval (f x)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
      a =
    (aeval (cfc (p := p) f a) : (a : R[X]) → A)
      (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
monomial :
  r • cfc (p := p) (fun (x : R) ↦ f x ^ (n + 1)) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a ^ (n + 1))
monomial₁ :
  r • cfc (p := p) f a ^ (n + 1) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a ^ (n + 1))
monomial₂ :
  r • cfc (p := p) f a ^ (n + 1) =
    HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a ^ (n + 1))
monomial₃ monomial₄ : r • cfc (p := p) f a ^ (n + 1) = r • cfc (p := p) f a ^ (n + 1)
⊢ cfc (p := p) (fun (x : R) ↦ r * f x ^ (n + 1)) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a ^ (n + 1))

Tactic:
rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]

Premises used: cfc_pow, algebraMap_smul, HAdd.hAdd, smul_eq_mul, OfNat.ofNat, cfc_const_mul
-- 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
q : R[X]
f : R → R
a : A
ha : p a
hf : ContinuousOn f (spectrum R a)
C :
  ∀ (r : R),
    cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) ((Polynomial.C : (a : R) → R[X]) r)) a =
      (aeval (cfc (p := p) f a) : (a : R[X]) → A) ((Polynomial.C : (a : R) → R[X]) r : R[X])
add :
  ∀ (q₁ q₂ : R[X])
    (hq₁ : cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q₁) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q₁)
    (hq₂ : cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q₂) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q₂),
    cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) (q₁ + q₂)) a =
      (aeval (cfc (p := p) f a) : (a : R[X]) → A) (q₁ + q₂)
monomial :
  ∀ (n : ℕ) (r : R),
    cfc (p := p)
          (fun (x : R) ↦
            Polynomial.eval (f x)
              (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
          a =
        (aeval (cfc (p := p) f a) : (a : R[X]) → A)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) →
      cfc (p := p)
          (fun (x : R) ↦
            Polynomial.eval (f x)
              (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))))
          a =
        (aeval (cfc (p := p) f a) : (a : R[X]) → A)
          (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q

Tactic:
induction q using Polynomial.induction_on with
  | C r => simp [cfc_const r a]
  | add q₁ q₂ hq₁ hq₂ =>
    simp only [eval_add, map_add, ← hq₁, ← hq₂, cfc_add a (q₁.eval <| f ·) (q₂.eval <| f ·)]
  | monomial n r _ =>
    simp only [eval_mul, eval_C, eval_X_pow, map_mul, aeval_C, map_pow, aeval_X]
    rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]

Premises used: Polynomial.eval_C, Polynomial.eval_X_pow, map_add, Polynomial.monomial, algebraMap_smul, Polynomial.eval_mul, map_pow, map_mul, Polynomial.aeval_C, Polynomial.eval_add, smul_eq_mul, Polynomial.aeval_X, cfc_const_mul
-- 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
q : R[X]
a : A
ha : p a
rw :
  Eq.{u_2 + 1} (α := A) ((aeval (cfc (p := p) (fun (x : R) ↦ x) a) : (a : R[X]) → A) q : A)
    ((aeval a : (a : R[X]) → A) q : A)
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((aeval a : (a : R[X]) → A) q : A) ((aeval a : (a : R[X]) → A) q : A)
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval x q) a = (aeval a : (a : R[X]) → A) q

Tactic:
rw [cfc_map_polynomial .., cfc_id' ..]

Premises used: cfc_id', cfc_map_polynomial
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
⊢ ContinuousOn (g ∘ f) (spectrum R a)

Tactic:
have := hg.comp hf <| (spectrum R a).mapsTo_image 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ p a

Tactic:
ha
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ p a

Tactic:
exact ha
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
rw :
  Set.range (ι := (↑(spectrum R a) : Type u_1))
      (⇑{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } :
        (a : (↑(spectrum R a) : Type u_1)) → R) =
    f '' spectrum R a
⊢ spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a

Tactic:
rw [cfcHom_map_spectrum (by exact ha) _]

Premises used: cfcHom_map_spectrum
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
h :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        (Set.range (ι := (↑(spectrum R a) : Type u_1))
          (⇑{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R))
        x ↔
      x ∈ f '' spectrum R a
⊢ Set.range (ι := (↑(spectrum R a) : Type u_1))
      (⇑{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } :
        (a : (↑(spectrum R a) : Type u_1)) → R) =
    f '' spectrum R a

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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
x : R
⊢ Membership.mem (γ := Set R)
      (Set.range (ι := (↑(spectrum R a) : Type u_1))
        (⇑{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
              C((↑(spectrum R a) : Type u_1), R) } :
          (a : (↑(spectrum R a) : Type u_1)) → R))
      x ↔
    x ∈ f '' spectrum R a

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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
⊢ spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a

Tactic:
have sp_eq : spectrum R (cfcHom (show p a from ha) (ContinuousMap.mk _ hf.restrict)) =
      f '' (spectrum R a) := by
    rw [cfcHom_map_spectrum (by exact ha) _]
    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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
⊢ ContinuousOn g (f '' spectrum R a)

Tactic:
hg
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
⊢ ContinuousOn g
    (spectrum.{u_1, u_2} R (A := 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))

Tactic:
convert! hg
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
x : (↑(spectrum R a) : Type u_1)
rw : (spectrum R a).restrict (π := fun (a : R) ↦ R) f x ∈ f '' spectrum R a
⊢ (spectrum R a).restrict (π := fun (a : R) ↦ R) f x ∈
    spectrum.{u_1, u_2} R (A := 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)

Tactic:
rw [sp_eq]
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
x : (↑(spectrum R a) : Type u_1)
h : (↑x : R) ∈ spectrum R a ∧ f (↑x : R) = (spectrum R a).restrict (π := fun (a : R) ↦ R) f x
⊢ (spectrum R a).restrict (π := fun (a : R) ↦ R) f x ∈ f '' spectrum R a

Tactic:
use x.1

Premises used: Subtype.val
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
x : (↑(spectrum R a) : Type u_1)
⊢ (↑x : R) ∈ spectrum R a ∧ f (↑x : R) = (spectrum R a).restrict (π := fun (a : R) ↦ R) f 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
⊢ C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := 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)) :
      Type u_1))

Tactic:
exact ContinuousMap.mk _ <| hf.restrict.codRestrict fun x ↦ by rw [sp_eq]; use x.1; simp

Premises used: ContinuousMap.mk, ContinuousOn.restrict, Continuous.codRestrict
-- 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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (g ∘ f), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (comp
          {
            toFun :=
              (spectrum.{u_1, u_2} R (A := 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)).restrict
                (π := fun (a : R) ↦ R) g,
            continuous_toFun := ⋯ }
          {
            toFun :=
              Set.codRestrict ((spectrum R a).restrict (π := fun (a : R) ↦ R) f)
                (spectrum.{u_1, u_2} R (A := 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))
                ⋯,
            continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1),
              (↑(spectrum.{u_1, u_2} R (A := 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)) :
                Type u_1)) }) :
      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
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := 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) =
    f '' spectrum R a
⊢ ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
              C((↑(spectrum R a) : Type u_1), R) } :
            (a : (↑(spectrum R a) : Type u_1)) → R)
          x :
        R)
      ((↑(({
                  toFun :=
                    Set.codRestrict ((spectrum R a).restrict (π := fun (a : R) ↦ R) f)
                      (spectrum.{u_1, u_2} R (A := 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))
                      ⋯,
                  continuous_toFun := ⋯ } :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R
                        ((cfcHom ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                          { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })) :
                    Type u_1))
              x) :
          R) :
        R)

Tactic:
fun _ ↦ rfl

Premises used: Set.restrict, rfl