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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (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) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ }) :
      A)
have pos : { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := sorry :
    C((↑(spectrum R a) : Type u_1), R) } =
  ∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := sorry }
Tactic: congr 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
⊢ { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯ :
      C((↑(spectrum R a) : Type u_1), R) } =
    ∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯ }
have pos : ∀ (a_1 : (↑(spectrum R a) : Type u_1)),
  Eq (α := R)
    (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := sorry :
            C((↑(spectrum R a) : Type u_1), R) } :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        a_1 :
      R)
    ((∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := sorry } :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        a_1 :
      R)
Tactic: ext
-- 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
have pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
Tactic: by_cases ha : p 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
⊢ cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
have neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
Tactic: by_cases ha : p 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ s • f x) a = s • cfc (p := p) f a
have pos : (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
    { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ s • f x, continuous_toFun := sorry :
      C((↑(spectrum R a) : Type u_1), R) } =
  HSMul.hSMul (β := A) s
    ((cfcHom (p := p) ha : (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)
Tactic: rw [cfc_apply f a, cfc_apply _ 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ s • f x, continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) } =
    HSMul.hSMul (β := A) s
      ((cfcHom (p := p) ha : (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 pos : (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
    { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := sorry :
      C((↑(spectrum R a) : Type u_1), R) } =
  HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
    ((cfcHom (p := p) ha : (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)
Tactic: simp_rw [← Pi.smul_def, ← smul_one_smul R s _]
-- 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) } =
    HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
      ((cfcHom (p := p) ha : (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 pos : 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) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (HSMul.hSMul (β := R) s 1 •
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) }) :
    A)
Tactic: rw [← map_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
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
Tactic: by_cases h : p a ∧ 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 : R → R
a : A
pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have neg : ∀ (h : ¬(p a ∧ ContinuousOn f (spectrum R a))), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
Tactic: by_cases h : p a ∧ ContinuousOn f (spectrum R a)
-- 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
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have ha : p a
Tactic: obtain ⟨ha, hf⟩ := h
Cleared hypotheses: h
-- 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
f : R → R
a : A
h : p a ∧ ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have hf : ContinuousOn f (spectrum R a)
Tactic: obtain ⟨ha, hf⟩ := h
Cleared hypotheses: h
-- 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)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have pos : 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) fun (x : R) ↦ star (f x), continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (star
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) }) :
    A)
Tactic: rw [cfc_apply f a, ← map_star, cfc_apply _ 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 : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
Tactic: obtain (ha | hf) := not_and_or.mp h
-- 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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have neg₁ : ∀ (hf : ¬ContinuousOn f (spectrum R a)), cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
Tactic: obtain (ha | hf) := not_and_or.mp h
-- 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
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ star (f x)) a = star (cfc (p := p) f a)
have neg : ¬ContinuousOn (Y := R) (fun (x : R) ↦ star (f x)) (spectrum R a)
Tactic: rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, star_zero]
-- 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
a : A
n : ℕ
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ x ^ n) a = a ^ n
have rw : cfc (p := p) (fun (x : R) ↦ x) a ^ n = a ^ n
Tactic: rw [cfc_pow .., 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
a : A
n : ℕ
ha : p a
rw : cfc (p := p) (fun (x : R) ↦ x) a ^ n = a ^ n
⊢ cfc (p := p) (fun (x : R) ↦ x ^ n) a = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [cfc_pow .., 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ s • x) a = s • a
have rw : s • cfc (p := p) (fun (x : R) ↦ x) a = s • a
Tactic: rw [cfc_smul .., 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
S : Type u_3
inst_9 : SMul S R
inst_10 : ContinuousConstSMul S R
inst_11 : SMulZeroClass S A
inst_12 : IsScalarTower S R A
inst_13 : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
rw : s • cfc (p := p) (fun (x : R) ↦ x) a = s • a
⊢ cfc (p := p) (fun (x : R) ↦ s • x) a = s • a
have rw₁ : s • a = s • a
Tactic: rw [cfc_smul .., 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
a : A
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ star x) a = star a
have rw : star (cfc (p := p) (fun (x : R) ↦ x) a) = star a
Tactic: rw [cfc_star .., 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
a : A
ha : p a
rw : star (cfc (p := p) (fun (x : R) ↦ x) a) = star a
⊢ cfc (p := p) (fun (x : R) ↦ star x) a = star a
have rw₁ : star a = star a
Tactic: rw [cfc_star .., 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
inst_9 : StarModule R A
a : A
ha : p a
⊢ (Set.range fun (x : R → R) ↦ cfc (p := p) x a) =
    (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
have h : ∀ (x : A),
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x ↔
    x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
Tactic: ext
-- 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 : StarModule R A
a : A
ha : p a
x : A
⊢ Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x ↔
    x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
have h : Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x →
  x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
Tactic: constructor
-- 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 : StarModule R A
a : A
ha : p a
x : A
h :
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x →
    x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
⊢ Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x ↔
    x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A)
have h₁ : x ∈ (↑(StarAlgHom.range (A := C((↑(spectrum R a) : Type u_1), R)) (cfcHom (p := p) ha)) : Set A) →
  Membership.mem (γ := Set A) (Set.range fun (x : R → R) ↦ cfc (p := p) x a) x
Tactic: constructor
-- 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))
⊢ 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)))
have 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))
Tactic: simp only [eval_mul, eval_C, eval_X_pow, map_mul, aeval_C, map_pow, aeval_X]
-- 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))
⊢ 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) (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))
Tactic: rw [cfc_const_mul .., cfc_pow _ (n + 1) _, ← smul_eq_mul, algebraMap_smul]