awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f 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 neg : ∀ (ha : ¬p a), cfc (p := p) f a = cfc (p := p) g a
Tactic: obtain (ha | hg) := 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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
neg : ∀ (ha : ¬p a), cfc (p := p) f a = cfc (p := p) g a
⊢ cfc (p := p) f a = cfc (p := p) g a
have neg₁ : ∀ (hg : ¬ContinuousOn g (spectrum R a)), cfc (p := p) f a = cfc (p := p) g a
Tactic: obtain (ha | hg) := 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 g : R → R
a : A
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
hg : ¬ContinuousOn g (spectrum R a)
⊢ cfc (p := p) f a = cfc (p := p) g a
have neg : ¬ContinuousOn f (spectrum R a)
Tactic: rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn]
-- 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 g : R → R
a : A
h : cfc (p := p) f a = cfc (p := p) g a
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ Set.EqOn f g (spectrum R a)
have h₁ : 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) g, continuous_toFun := sorry :
        C((↑(spectrum R a) : Type u_1), R) } :
    A)
Tactic: rw [cfc_apply f a, cfc_apply g a] 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
a : A
⊢ cfc.{u_1, u_2} (R := R) (p := p) 0 a = 0
have pos : ∀ (ha : p a), cfc.{u_1, u_2} (R := R) (p := p) 0 a = 0
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
a : A
pos : ∀ (ha : p a), cfc.{u_1, u_2} (R := R) (p := p) 0 a = 0
⊢ cfc.{u_1, u_2} (R := R) (p := p) 0 a = 0
have neg : ∀ (ha : ¬p a), cfc.{u_1, u_2} (R := R) (p := p) 0 a = 0
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
a : A
ha : ¬p a
⊢ cfc.{u_1, u_2} (R := R) (p := p) 0 a = 0
have neg : Eq.{u_2 + 1} (α := A) 0 0
Tactic: rw [cfc_apply_of_not_predicate a 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)
hg : ContinuousOn g (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ f x * g x) a = cfc (p := p) f a * cfc (p := p) g a
have pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ f x * g x) a = cfc (p := p) f a * cfc (p := p) g 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
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ f x * g x) a = cfc (p := p) f a * cfc (p := p) g a
⊢ cfc (p := p) (fun (x : R) ↦ f x * g x) a = cfc (p := p) f a * cfc (p := p) g a
have neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ f x * g x) a = cfc (p := p) f a * cfc (p := p) g 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
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f x * g x) a = cfc (p := p) f a * cfc (p := p) g 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) ↦ f x * g 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)
      ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) } *
        { 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 f a, cfc_apply g a, ← map_mul, 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
n : ℕ
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f x ^ n) a = cfc (p := p) f a ^ n
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) ↦ f x ^ n, 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) } ^
        n) :
    A)
Tactic: rw [cfc_apply f a, ← map_pow, 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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
⊢ cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g a
have pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g 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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
pos : ∀ (ha : p a), cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g a
⊢ cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g a
have neg : ∀ (ha : ¬p a), cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g 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
a : A
f g : R → R
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f x + g x) a = cfc (p := p) f a + cfc (p := p) g 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) ↦ f x + g 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)
      ({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
          C((↑(spectrum R a) : Type u_1), R) } +
        { 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 f a, cfc_apply g a, ← map_add, 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z
have h : ∀ (x : R), r + f x = (fun (x : R) ↦ r) x + f 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
have this : Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z
Tactic: have : (fun z => r + f z) = (fun z => (fun _ => r) z + f z) := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
this : Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z
rw :
  cfc (p := p) (fun (z : R) ↦ (fun (x : R) ↦ r) z + f z) a =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
have rw₁ : cfc (p := p) (fun (x : R) ↦ r) a + cfc (p := p) f a =
  HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
Tactic: rw [this, cfc_add a _ _ (continuousOn_const (c := r)) hf, cfc_const r a 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
this : Eq.{u_1 + 1} (α := (z : R) → R) (fun (z : R) ↦ r + f z) fun (z : R) ↦ (fun (x : R) ↦ r) z + f z
rw :
  cfc (p := p) (fun (z : R) ↦ (fun (x : R) ↦ r) z + f z) a =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
rw₁ :
  cfc (p := p) (fun (x : R) ↦ r) a + cfc (p := p) f a =
    HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
⊢ cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
have rw₂ : HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a) =
  HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
Tactic: rw [this, cfc_add a _ _ (continuousOn_const (c := r)) hf, cfc_const r a 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f x + r) a = HAdd.hAdd (β := A) (cfc (p := p) f a) ((algebraMap R A : (a : R) → A) r : A)
have rw : cfc (p := p) (fun (x : R) ↦ f x + r) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
Tactic: rw [add_comm (cfc f 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
r : R
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
| cfc (p := p) (fun (x : R) ↦ f x + r) a
have simp : cfc (p := p) (fun (x : R) ↦ r + f x) a
Tactic: simp only [add_comm]
-- 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
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ cfc (p := p) (fun (x : R) ↦ f x + r) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
have conv_lhs : cfc (p := p) (fun (x : R) ↦ r + f x) a = HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) r : A) (cfc (p := p) f a)
Tactic: conv_lhs => simp only [add_comm]
-- 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)
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
have pos : ∀ (ha : p a), cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
pos : ∀ (ha : p a), cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
have neg : ∀ (ha : ¬p a), cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
⊢ s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
have h : ∀ (x : R), s.sum f x = ∑ i ∈ s, f i 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
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (spectrum R a)
ha : p a
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
have hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
Tactic: have hsum : s.sum f = fun z => ∑ i ∈ s, f i z := by ext; simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
ι : 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
⊢ ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
have rw : ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (spectrum R a)
Tactic: rw [sum_coe_sort s, hsum]
-- 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
ι : 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
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
have hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (spectrum R a)
Tactic: have hf' : ContinuousOn (∑ i : s, f i) (spectrum R a) := by
      rw [sum_coe_sort s, hsum]
      exact continuousOn_finsetSum s fun i hi => hf i hi
-- 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)
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i ∈ s, f i) a = ∑ i ∈ s, cfc (p := p) (f i) a
have pos : cfc.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfc (p := p) (f (↑i : ι)) a
Tactic: rw [← sum_coe_sort s, ← sum_coe_sort 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
ι : 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)
⊢ cfc.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfc (p := p) (f (↑i : ι)) 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) (∑ i : ↥s, f (↑i : ι)), 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)
      (∑ x : ↥s, { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := sorry }) :
    A)
Tactic: rw [cfc_apply_pi _ a ha (fun ⟨i, hi⟩ => hf i hi), ← map_sum, cfc_apply _ a ha hf']