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
f : R → R
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)
    (((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) } :
      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)
  ((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)
  (((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]
-- 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)
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)
    (((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) } :
      A)
rw₁ :
  Eq.{u_2 + 1} (α := 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)
    (((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) } :
      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)
  ((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⟩, cfcL_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
f : R → R
a : A
ha : p a
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
have pos : ∀ (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)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
Tactic: by_cases hf : 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
ha : p a
pos :
  ∀ (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)
        (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
have neg : ∀ (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)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
Tactic: by_cases hf : 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
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)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
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) 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)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0) :
    A)
Tactic: rw [cfc_apply f a, mkD_of_continuousOn 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)
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) f, 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)
        (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0) :
      A)
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
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) 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_apply f a, mkD_of_continuousOn 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)
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
have neg : Eq.{u_2 + 1} (α := A) (0 : A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0) :
    A)
Tactic: rw [cfc_apply_of_not_continuousOn a hf, mkD_of_not_continuousOn hf,
      map_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
f : R → R
a : A
ha : p a
hf : ¬ContinuousOn f (spectrum R a)
neg :
  Eq.{u_2 + 1} (α := A) (0 : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0) :
      A)
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
have neg₁ : Eq.{u_2 + 1} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) 0 : A)
Tactic: rw [cfc_apply_of_not_continuousOn a hf, mkD_of_not_continuousOn hf,
      map_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
f : R → R
a : A
ha : p a
hf : ¬ContinuousOn f (spectrum R a)
neg :
  Eq.{u_2 + 1} (α := A) (0 : A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0) :
      A)
neg₁ : Eq.{u_2 + 1} (α := A) (0 : A) ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A) 0 : A)
⊢ cfc (p := p) f a =
    (cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      (mkD ((spectrum R a).restrict (π := fun (a : R) ↦ R) f) 0)
have neg₂ : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfc_apply_of_not_continuousOn a hf, mkD_of_not_continuousOn hf,
      map_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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P
      ((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) })
⊢ P (cfc (p := p) f a)
have pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), P (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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P
      ((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) })
pos : ∀ (h : p a ∧ ContinuousOn f (spectrum R a)), P (cfc (p := p) f a)
⊢ P (cfc (p := p) f a)
have neg : ∀ (h : ¬(p a ∧ ContinuousOn f (spectrum R a))), P (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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P
      ((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) })
h : p a ∧ ContinuousOn f (spectrum R a)
⊢ P (cfc (p := p) f a)
have pos : P
  ((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) })
Tactic: rw [cfc_apply f a h.1 h.2]
-- 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P
      ((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) })
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ P (cfc (p := p) f a)
have h₁ : ¬p a ∨ ¬ContinuousOn f (spectrum R a)
Tactic: simp only [not_and_or] at 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P
      ((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) })
h : ¬p a ∨ ¬ContinuousOn f (spectrum R a)
⊢ P (cfc (p := p) f a)
have neg : ∀ (h : ¬p a), P (cfc (p := p) f a)
Tactic: obtain (h | h) := 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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P
      ((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) })
h : ¬p a ∨ ¬ContinuousOn f (spectrum R a)
neg : ∀ (h : ¬p a), P (cfc (p := p) f a)
⊢ P (cfc (p := p) f a)
have neg₁ : ∀ (h : ¬ContinuousOn f (spectrum R a)), P (cfc (p := p) f a)
Tactic: obtain (h | h) := 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 g : R → R
a : A
⊢ Commute (cfc (p := p) f a) (cfc (p := p) g a)
have refine : ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
  (fun (x : A) ↦ Commute x (cfc (p := p) g 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) })
Tactic: refine cfc_cases (fun x ↦ Commute x (cfc g a)) a f (by simp) fun hf 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 g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (fun (x : A) ↦ Commute x (cfc (p := p) g 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 refine : ∀ (hg : ContinuousOn g (spectrum R a)) (x : p a),
  (fun (x : A) ↦
      Commute
        ((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) })
        x)
    ((cfcHom (p := p) x : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) })
Tactic: refine cfc_cases (fun x ↦ Commute _ x) a g (by simp) fun hg _ ↦ ?_
-- 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
a : A
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ r) a = (algebraMap R A : (a : R) → A) r
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) fun (x : R) ↦ r, continuous_toFun := sorry } :
    A)
  ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      ((algebraMap R C((↑(spectrum R a) : Type u_1), R) : (a_1 : R) → C((↑(spectrum R a) : Type u_1), R)) r :
        C((↑(spectrum R a) : Type u_1), R)) :
    A)
Tactic: rw [cfc_apply (fun _ : R ↦ r) a, ← AlgHomClass.commutes (cfcHom ha (p := p)) 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
f g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
⊢ cfc (p := p) f a = cfc (p := p) g a
have pos : ∀ (h : p a ∧ ContinuousOn g (spectrum R a)), cfc (p := p) f a = cfc (p := p) g a
Tactic: by_cases h : p a ∧ ContinuousOn g (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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
pos : ∀ (h : p a ∧ ContinuousOn g (spectrum R a)), cfc (p := p) f a = cfc (p := p) g a
⊢ cfc (p := p) f a = cfc (p := p) g a
have neg : ∀ (h : ¬(p a ∧ ContinuousOn g (spectrum R a))), cfc (p := p) f a = cfc (p := p) g a
Tactic: by_cases h : p a ∧ ContinuousOn g (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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ cfc (p := p) f a = cfc (p := p) g a
have pos : 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) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
Tactic: rw [cfc_apply (ha := h.1) (hf := h.2.congr hfg), cfc_apply (ha := h.1) (hf := h.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 : 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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : p a ∧ ContinuousOn g (spectrum R a)
⊢ Eq.{u_2 + 1} (α := 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)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
have pos : (spectrum R a).restrict (π := fun (a : R) ↦ R) f = (spectrum R a).restrict (π := fun (a : R) ↦ R) g
Tactic: congr 2