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
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
refine_1 :
  Continuous[_, inst_5]
    (⇑φ : (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)
⊢ cfcHom (p := p) ⋯ = φ
have refine_2 : Eq.{u_2 + 1} (α := A)
  ((φ : (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)
      (restrict
        (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
        (ContinuousMap.id R)) :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
Tactic: refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha 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
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1), R)) → A)
        (restrict
          (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
          (ContinuousMap.id R)) :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
have refine_2 : Eq.{u_2 + 1} (α := A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (comp
        (restrict
          (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
          (ContinuousMap.id R))
        f') :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
Tactic: simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply]
-- 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
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (comp
          (restrict
            (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
            (ContinuousMap.id R))
          f') :
      A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
have refine_2 : comp
    (restrict
      (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
      (ContinuousMap.id R))
    f' =
  f
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
a : A
ha : p a
inst_9 : UniqueHom R A
f : C((↑(spectrum R a) : Type u_1), R)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R ((cfcHom ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R)
φ : C((↑(spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)) :
      Type u_1),
    R) →⋆ₐ[R]
  A :=
  StarAlgHom.comp (cfcHom (p := p) ha) (compStarAlgHom' R R f')
⊢ comp
      (restrict
        (spectrum.{u_1, u_2} R (A := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
        (ContinuousMap.id R))
      f' =
    f
have refine_2 : ∀ (x : (↑(spectrum R a) : Type u_1)),
  Eq (α := R)
    ((comp
            (restrict
              (spectrum.{u_1, u_2} R (A := A)
                ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A))
              (ContinuousMap.id R))
            f' :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        x :
      R)
    ((f : (a : (↑(spectrum R a) : Type u_1)) → R) x : R)
Tactic: ext 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)
⊢ cfc (p := p) f a =
    (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) }
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (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) }
    else 0 :
    A)
  ((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_def, dif_pos ⟨ha, hf⟩]
-- 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)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
        (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) }
      else 0 :
      A)
    ((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)
⊢ cfc (p := p) f a =
    (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) }
have rw₁ : Eq.{u_2 + 1} (α := 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)
  ((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_def, dif_pos ⟨ha, hf⟩]
-- 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
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (spectrum R a)
⊢ Eq (α := (i : ι) → A) (fun (i : ι) ↦ cfc (p := p) (f i) a) fun (i : ι) ↦
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯ :
        C((↑(spectrum R a) : Type u_1), R) }
have h : ∀ (i : ι),
  cfc (p := p) (f i) a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) }
Tactic: ext i
-- 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 ∧ ContinuousOn f (spectrum R a))
⊢ cfc (p := p) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (spectrum R a) then
    (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) }
  else 0)
  0
Tactic: rw [cfc_def, dif_neg 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
f : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (spectrum R a))
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (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) }
    else 0)
    0
⊢ cfc (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfc_def, dif_neg 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
f : R → R
a : A
ha : ¬p a
⊢ cfc (p := p) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (spectrum R a) then
    (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) }
  else 0)
  0
Tactic: rw [cfc_def, dif_neg (not_and_of_not_left _ 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
f : R → R
a : A
ha : ¬p a
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (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) }
    else 0)
    0
⊢ cfc (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfc_def, dif_neg (not_and_of_not_left _ 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
f : R → R
a : A
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc (p := p) f a = 0
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (spectrum R a) then
    (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) }
  else 0)
  0
Tactic: rw [cfc_def, dif_neg (not_and_of_not_right _ hf)]
-- 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
hf : ¬ContinuousOn f (spectrum R a)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (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) }
    else 0)
    0
⊢ cfc (p := p) f a = 0
have rw₁ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfc_def, dif_neg (not_and_of_not_right _ hf)]
-- 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
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
have h : ∀ (x : (↑(spectrum R a) : Type u_1)),
  (f : (a : (↑(spectrum R a) : Type u_1)) → R) x =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
      x
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
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f =
    cfc (p := p)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
      a
have h : (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
  (spectrum R a).restrict (π := fun (a : R) ↦ R)
    (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
      (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
Tactic: have h : f = (spectrum R a).restrict (Function.extend Subtype.val f g) := by
    ext; simp
-- 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
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h :
  (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f =
    cfc (p := p)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
      a
have hg : ContinuousOn
  (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
    (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
  (spectrum R a)
Tactic: have hg : ContinuousOn (Function.extend Subtype.val f g) (spectrum R a) :=
    continuousOn_iff_continuous_restrict.mpr <| h ▸ map_continuous 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
a : A
g : R → R
ha : p a
f : C((↑(spectrum R a) : Type u_1), R)
h :
  (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) =
    (spectrum R a).restrict (π := fun (a : R) ↦ R)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
hg :
  ContinuousOn
    (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
      (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
    (spectrum R a)
⊢ (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f =
    cfc (p := p)
      (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
        (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g)
      a
have rw : Eq.{u_2 + 1} (α := A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) f : A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      {
        toFun :=
          (spectrum R a).restrict (π := fun (a : R) ↦ R)
            (Function.extend (α := { x : R // x ∈ spectrum R a }) (Subtype.val (p := fun (x : R) ↦ x ∈ spectrum R a))
              (⇑f : (a : (↑(spectrum R a) : Type u_1)) → R) g),
        continuous_toFun := sorry : C((↑(spectrum R a) : Type u_1), R) } :
    A)
Tactic: rw [cfc_apply ..]
-- 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
f : R → R
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc (p := p) f a =
    ((cfcL (p := p) ha : C((↑(spectrum R a) : Type u_1), R) →L[R] A) : (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) }
have rw : Eq.{u_2 + 1} (α := A)
  (if h : p a ∧ ContinuousOn f (spectrum R a) then
      (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) }
    else 0 :
    A)
  (((cfcL (p := p) ha : C((↑(spectrum R a) : Type u_1), R) →L[R] A) : (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_def, dif_pos ⟨ha, hf⟩, cfcL_apply]