awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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))
⊢ 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))
have 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))
Tactic: rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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))
⊢ 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))
have 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))
Tactic: rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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))
⊢ 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))
have monomial₃ : r • cfc (p := p) f a ^ (n + 1) = r • cfc (p := p) f a ^ (n + 1)
Tactic: rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q
have 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])
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]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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])
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q
have 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₂)
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]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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₂)
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval (f x) q) a = (aeval (cfc (p := p) f a) : (a : R[X]) → A) q
have 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)))
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]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval x q) a = (aeval a : (a : R[X]) → A) q
have 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)
Tactic: rw [cfc_map_polynomial .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ cfc (p := p) (fun (x : R) ↦ Polynomial.eval x q) a = (aeval a : (a : R[X]) → A) q
have rw₁ : Eq.{u_2 + 1} (α := A) ((aeval a : (a : R[X]) → A) q : A) ((aeval a : (a : R[X]) → A) q : A)
Tactic: rw [cfc_map_polynomial .., cfc_id' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
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)
⊢ cfc (p := p) (g ∘ f) a = cfc (p := p) g (cfc (p := p) f a)
have this : ContinuousOn (g ∘ f) (spectrum R a)
Tactic: have := hg.comp hf <| (spectrum R a).mapsTo_image f
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
have rw : Set.range (ι := (↑(spectrum R a) : Type u_1))
    (⇑{ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) } :
      (a : (↑(spectrum R a) : Type u_1)) → R) =
  f '' spectrum R a
Tactic: rw [cfcHom_map_spectrum (by exact ha) _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ 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
have 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 := sorry :
              C((↑(spectrum R a) : Type u_1), R) } :
          (a : (↑(spectrum R a) : Type u_1)) → R))
      x ↔
    x ∈ f '' spectrum R a
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (hypothesis)
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)
⊢ cfc (p := p) (g ∘ f) a = cfc (p := p) g (cfc (p := p) f a)
have sp_eq : spectrum.{u_1, u_2} R (A := A)
    ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
⊢ cfc (p := p) (g ∘ f) a = cfc (p := p) g (cfc (p := p) f a)
have rw : 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 := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (comp
        {
          toFun :=
            (spectrum.{u_1, u_2} R (A := A)
                  ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
                        C((↑(spectrum R a) : Type u_1), R) } :
                    A)).restrict
              (π := fun (a : R) ↦ R) g,
          continuous_toFun := sorry }
        {
          toFun :=
            Set.codRestrict ((spectrum R a).restrict (π := fun (a : R) ↦ R) f)
              (spectrum.{u_1, u_2} R (A := A)
                ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                    { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
                      C((↑(spectrum R a) : Type u_1), R) } :
                  A))
              sorry,
          continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1),
            (↑(spectrum.{u_1, u_2} R (A := A)
                  ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
                        C((↑(spectrum R a) : Type u_1), R) } :
                    A)) :
              Type u_1)) }) :
    A)
Tactic: rw [cfc_apply .., cfc_apply f a,
    cfc_apply _ _ (cfcHom_predicate (show p a from ha) _) (by convert! hg), ← cfcHom_comp _ _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
rw :
  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)
⊢ cfc (p := p) (g ∘ f) a = cfc (p := p) g (cfc (p := p) f a)
have f' : C((↑(spectrum R a) : Type u_1),
  (↑(spectrum.{u_1, u_2} R (A := A)
        ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
            { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
              C((↑(spectrum R a) : Type u_1), R) } :
          A)) :
    Type u_1))
Tactic: rw [cfc_apply .., cfc_apply f a,
    cfc_apply _ _ (cfcHom_predicate (show p a from ha) _) (by convert! hg), ← cfcHom_comp _ _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ (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)
have rw : (spectrum R a).restrict (π := fun (a : R) ↦ R) f x ∈ f '' spectrum R a
Tactic: rw [sp_eq]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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)
⊢ (spectrum R a).restrict (π := fun (a : R) ↦ R) f x ∈ f '' spectrum R a
have h : (↑x : R) ∈ spectrum R a ∧ f (↑x : R) = (spectrum R a).restrict (π := fun (a : R) ↦ R) f x
Tactic: use x.1
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
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
f : R → R
n : ℕ
a : A
hf : ContinuousOn f ((fun (x : R) ↦ x ^ n) '' spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f (x ^ n)) a = cfc (p := p) f (a ^ n)
have rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ x ^ n) a) = cfc (p := p) f (a ^ n)
Tactic: rw [cfc_comp' .., cfc_pow_id ..]