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
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
rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ x ^ n) a) = cfc (p := p) f (a ^ n)
⊢ cfc (p := p) (fun (x : R) ↦ f (x ^ n)) a = cfc (p := p) f (a ^ n)
have rw₁ : cfc (p := p) f (a ^ n) = cfc (p := p) f (a ^ n)
Tactic: rw [cfc_comp' .., cfc_pow_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
inst_9 : UniqueHom R A
S : Type u_3
inst_10 : SMul S R
inst_11 : ContinuousConstSMul S R
inst_12 : SMulZeroClass S A
inst_13 : IsScalarTower S R A
inst_14 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ s • x) '' spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f (s • x)) a = cfc (p := p) f (s • a)
have rw : cfc (p := p) f (cfc (p := p) (HSMul.hSMul s) a) = cfc (p := p) f (s • a)
Tactic: rw [cfc_comp' .., cfc_smul_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
inst_9 : UniqueHom R A
S : Type u_3
inst_10 : SMul S R
inst_11 : ContinuousConstSMul S R
inst_12 : SMulZeroClass S A
inst_13 : IsScalarTower S R A
inst_14 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ s • x) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (HSMul.hSMul s) a) = cfc (p := p) f (s • a)
⊢ cfc (p := p) (fun (x : R) ↦ f (s • x)) a = cfc (p := p) f (s • a)
have rw₁ : cfc (p := p) f (s • a) = cfc (p := p) f (s • a)
Tactic: rw [cfc_comp' .., cfc_smul_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
inst_9 : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ r * x) '' spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f (r * x)) a = cfc (p := p) f (r • a)
have rw : cfc (p := p) f (cfc (p := p) (HMul.hMul r) a) = cfc (p := p) f (r • a)
Tactic: rw [cfc_comp' .., cfc_const_mul_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
inst_9 : UniqueHom R A
r : R
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ r * x) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (HMul.hMul r) a) = cfc (p := p) f (r • a)
⊢ cfc (p := p) (fun (x : R) ↦ f (r * x)) a = cfc (p := p) f (r • a)
have rw₁ : cfc (p := p) f (r • a) = cfc (p := p) f (r • a)
Tactic: rw [cfc_comp' .., cfc_const_mul_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
inst_9 : UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (star '' spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f (star x)) a = cfc (p := p) f (star a)
have rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) star a) = cfc (p := p) f (star a)
Tactic: rw [cfc_comp' .., cfc_star_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
inst_9 : UniqueHom R A
f : R → R
a : A
hf : ContinuousOn f (star '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc.{u_1, u_2} (R := R) (p := p) star a) = cfc (p := p) f (star a)
⊢ cfc (p := p) (fun (x : R) ↦ f (star x)) a = cfc (p := p) f (star a)
have rw₁ : cfc (p := p) f (star a) = cfc (p := p) f (star a)
Tactic: rw [cfc_comp' .., cfc_star_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
inst_9 : UniqueHom R A
q : R[X]
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ Polynomial.eval x q) '' spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f (Polynomial.eval x q)) a = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
have rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ Polynomial.eval x q) a) = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
Tactic: rw [cfc_comp' .., cfc_polynomial ..]
-- 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
q : R[X]
f : R → R
a : A
hf : ContinuousOn f ((fun (x : R) ↦ Polynomial.eval x q) '' spectrum R a)
ha : p a
rw : cfc (p := p) f (cfc (p := p) (fun (x : R) ↦ Polynomial.eval x q) a) = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
⊢ cfc (p := p) (fun (x : R) ↦ f (Polynomial.eval x q)) a = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
have rw₁ : cfc (p := p) f ((aeval a : (a : R[X]) → A) q) = cfc (p := p) f ((aeval a : (a : R[X]) → A) q)
Tactic: rw [cfc_comp' .., cfc_polynomial ..]
-- 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
r : R
⊢ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A) ⊆ {r}
have rw : Subset (α := Set R) ((fun (x : R) ↦ r) '' spectrum.{u_1, u_2} R (A := A) 0) {r}
Tactic: rw [← cfc_const r 0 (cfc_predicate_zero R),
    cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]
-- 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 : Nontrivial A
r : R
⊢ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A) = {r}
have hp : p 0
Tactic: have hp : p 0 := cfc_predicate_zero R
-- 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 : Nontrivial A
r : R
hp : p 0
⊢ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A) = {r}
have rw : Eq (α := Set R) ((fun (x : R) ↦ r) '' spectrum.{u_1, u_2} R (A := A) 0) {r}
Tactic: rw [← cfc_const r 0 hp, cfc_map_spectrum (fun _ => r) 0 hp]
-- 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 : Nontrivial A
⊢ spectrum.{u_1, u_2} R (A := A) 0 = {0}
have this : Eq.{u_2 + 1} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) 0 : A)
Tactic: have : (0 : A) = algebraMap R A 0 := Eq.symm (map_zero (algebraMap R A))
-- 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 : Nontrivial A
this : Eq.{u_2 + 1} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) 0 : A)
⊢ spectrum.{u_1, u_2} R (A := A) 0 = {0}
have rw : spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) 0 : A) = {0}
Tactic: rw [this, spectrum_algebraMap_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 : Nontrivial A
this : Eq.{u_2 + 1} (α := A) (0 : A) ((algebraMap R A : (a : R) → A) 0 : A)
rw : spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) 0 : A) = {0}
⊢ spectrum.{u_1, u_2} R (A := A) 0 = {0}
have rw₁ : Eq (α := Set R) {0} {0}
Tactic: rw [this, spectrum_algebraMap_eq]
-- 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 : Nontrivial A
⊢ spectrum.{u_1, u_2} R (A := A) 1 = {1}
have this : Eq.{u_2 + 1} (α := A) (1 : A) ((algebraMap R A : (a : R) → A) 1 : A)
Tactic: have : (1 : A) = algebraMap R A 1 := Eq.symm (map_one (algebraMap R A))
-- 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 : Nontrivial A
this : Eq.{u_2 + 1} (α := A) (1 : A) ((algebraMap R A : (a : R) → A) 1 : A)
⊢ spectrum.{u_1, u_2} R (A := A) 1 = {1}
have rw : spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A) = {1}
Tactic: rw [this, spectrum_algebraMap_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 : Nontrivial A
this : Eq.{u_2 + 1} (α := A) (1 : A) ((algebraMap R A : (a : R) → A) 1 : A)
rw : spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) 1 : A) = {1}
⊢ spectrum.{u_1, u_2} R (A := A) 1 = {1}
have rw₁ : Eq (α := Set R) {1} {1}
Tactic: rw [this, spectrum_algebraMap_eq]
-- 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
r : R
f : R → R
⊢ cfc (p := p) f ((algebraMap R A : (a : R) → A) r) = (algebraMap R A : (a : R) → A) (f r)
have h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
Tactic: have h₁ : ContinuousOn f (spectrum R (algebraMap R A r)) :=
  continuousOn_singleton _ _ |>.mono <| CFC.spectrum_algebraMap_subset r
-- 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
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
⊢ cfc (p := p) f ((algebraMap R A : (a : R) → A) r) = (algebraMap R A : (a : R) → A) (f r)
have rw : Eq.{u_2 + 1} (α := A)
  ((cfcHom (p := p) sorry : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
      {
        toFun :=
          (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f,
        continuous_toFun := sorry :
        C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) sorry : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
      ((algebraMap R C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) :
            (a : R) → C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R))
          (f r) :
        C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R)) :
    A)
Tactic: rw [cfc_apply f (algebraMap R A r) (cfc_predicate_algebraMap r),
    ← AlgHomClass.commutes (cfcHom (p := p) (cfc_predicate_algebraMap r)) (f r)]
-- 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
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
        {
          toFun :=
            (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f,
          continuous_toFun := ⋯ :
          C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R)) → A)
        ((algebraMap R C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R) :
              (a : R) → C((↑(spectrum R ((algebraMap R A : (a : R) → A) r)) : Type u_1), R))
            (f r) :
          C((↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1), R)) :
      A)
have h : (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f =
  fun (x : (↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1)) ↦
  (algebraMap R R : (a : R) → R) (f r)
Tactic: congr
-- 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
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
⊢ (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f =
    fun (x : (↑(spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) : Type u_1)) ↦
    (algebraMap R R : (a : R) → R) (f r)
have h : ∀ (x : R) (hx : x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)),
  (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f
      (Subtype.mk (p := fun (x : R) ↦ x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) x hx) =
    (algebraMap R R : (a : R) → R) (f r)
Tactic: ext ⟨x, hx⟩
-- 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
r : R
f : R → R
h₁ : ContinuousOn f (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A))
x : R
hx : x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)
⊢ (spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)).restrict (π := fun (a : R) ↦ R) f
      (Subtype.mk (p := fun (x : R) ↦ x ∈ spectrum.{u_1, u_2} R (A := A) ((algebraMap R A : (a : R) → A) r : A)) x hx) =
    (algebraMap R R : (a : R) → R) (f r)
have hx₁ : Membership.mem (γ := Set R) {r} x
Tactic: apply CFC.spectrum_algebraMap_subset r at hx
-- 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_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
have pos : ∀ (h : ContinuousOn f (spectrum R a)),
  star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
Tactic: by_cases h : ContinuousOn f (spectrum R a)
-- 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_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
pos :
  ∀ (h : ContinuousOn f (spectrum R a)),
    star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
have neg : ∀ (h : ¬ContinuousOn f (spectrum R a)),
  star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
Tactic: by_cases h : ContinuousOn f (spectrum R a)
-- 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_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ContinuousOn f (spectrum R a)
⊢ star (cfc (p := p) f a) * cfc (p := p) f a = cfc (p := p) f a * star (cfc (p := p) f a)
have pos : cfc (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfc (p := p) (fun (x : R) ↦ f x * star (f x)) a
Tactic: rw [← cfc_star, ← cfc_mul .., ← cfc_mul ..]
-- 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_1 g : R → R
a_1 : A
ha : p a_1
hf : ContinuousOn f_1 (spectrum R a_1)
hg : ContinuousOn g (spectrum R a_1)
f : R → R
a : A
h : ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfc (p := p) (fun (x : R) ↦ f x * star (f x)) a
have pos : ∀ (x : R), star (f x) * f x = f x * star (f x)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ IsUnit (cfc (p := p) f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0
have rw : 0 ∉ f '' spectrum R a ↔ ∀ x ∈ spectrum R a, f x ≠ 0
Tactic: rw [← spectrum.zero_notMem_iff R, cfc_map_spectrum ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
inst_10 : ContinuousInv₀ R
f : R → R
a : A
hf' : ∀ x ∈ spectrum R a, f x ≠ 0
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) f a * cfc (p := p) (fun (x : R) ↦ (f x)⁻¹) a = 1
have rw : cfc (p := p) (fun (x : R) ↦ f x * (f x)⁻¹) a = cfc.{u_1, u_2} (R := R) (p := p) 1 a
Tactic: rw [← cfc_mul .., ← cfc_one R a]