awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
pos :
  (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x + g x, continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HAdd.hAdd (α := A) (β := A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x + g x) a = cfcₙ (p := p) f a + cfcₙ (p := p) g a

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a, cfcₙ_apply _ a]

Premises used: cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x + g x, continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (HAdd.hAdd (α := C((↑(σₙ R a) : Type u_1), R)₀)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }) :
      A)
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x + g x, continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HAdd.hAdd (α := A) (β := A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)

Tactic:
simp_rw [← map_add]

Premises used: map_add
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x + g x, continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (HAdd.hAdd (α := C((↑(σₙ R a) : Type u_1), R)₀)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }) :
      A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
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:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
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
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
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
h : ∀ (x : R), s.sum f x = ∑ i ∈ s, f i x
⊢ s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
x : R
⊢ s.sum f x = ∑ i ∈ s, f i x

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
rw : ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (σₙ R a)
⊢ ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)

Tactic:
rw [sum_coe_sort s, hsum]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
⊢ ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (σₙ R a)

Tactic:
continuousOn_finsetSum s fun i hi => hf i hi

Premises used: continuousOn_finsetSum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
⊢ ContinuousOn (Y := R) (fun (z : R) ↦ ∑ i ∈ s, f i z) (σₙ R a)

Tactic:
exact continuousOn_finsetSum s fun i hi => hf i hi

Premises used: continuousOn_finsetSum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
⊢ ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)

Tactic:
have hf' : ContinuousOn (∑ i : s, f i) (σₙ R a) := by
      rw [sum_coe_sort s, hsum]
      exact continuousOn_finsetSum s fun i hi => hf i hi
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
pos : 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

Tactic:
rw [← sum_coe_sort s, ← sum_coe_sort s]

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (∑ x : ↥s,
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
⊢ cfcₙ.{u_1, u_2} (R := R) (p := p) (∑ i : ↥s, f (↑i : ι)) a = ∑ i : ↥s, cfcₙ (p := p) (f (↑i : ι)) a

Tactic:
rw [cfcₙ_apply_pi _ a ha (fun ⟨i, hi⟩ => hf i hi), ← map_sum, cfcₙ_apply _ a hf']

Premises used: map_sum, cfcₙ_apply_pi, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
pos :
  Eq (α := C((↑(σₙ R a) : Type u_1), R)₀)
    { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯, map_zero' := ⋯ }
    (∑ x : ↥s,
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ })
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (∑ x : ↥s,
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)

Tactic:
congr 1
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
pos :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R)
      (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯,
              map_zero' := ⋯ } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          x :
        R)
      ((∑ x : ↥s,
              { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯,
                map_zero' := ⋯ } :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          x :
        R)
⊢ Eq (α := C((↑(σₙ R a) : Type u_1), R)₀)
    { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯, map_zero' := ⋯ }
    (∑ x : ↥s,
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
ha : p a
hsum : s.sum f = fun (z : R) ↦ ∑ i ∈ s, f i z
hf' : ContinuousOn (Y := R) (∑ i : ↥s, f (↑i : ι)) (σₙ R a)
x : (↑(σₙ R a) : Type u_1)
⊢ Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (∑ i : ↥s, f (↑i : ι)), continuous_toFun := ⋯,
            map_zero' := ⋯ } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)
    ((∑ x : ↥s,
            { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f (↑x : ι)), continuous_toFun := ⋯, map_zero' := ⋯ } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
f : ι → R → R
a : A
s : Finset ι
hf : ∀ i ∈ s, ContinuousOn (f i) (σₙ R a)
hf0 : ∀ i ∈ s, f i 0 = 0
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:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
ι : Type u_3
inst_12 : Fintype ι
f : ι → R → R
a : A
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
⊢ cfcₙ.{u_1, u_2} (R := R) (p := p) (∑ i : ι, f i) a = ∑ i : ι, cfcₙ (p := p) (f i) a

Tactic:
cfcₙ_sum f a _ (fun i _ ↦ hf i) (fun i _ ↦ hf0 i)

Premises used: cfcₙ_sum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
pos : ∀ (ha : p a), cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a
neg : ∀ (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

Tactic:
by_cases ha : p a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
pos :
  (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ s • f x, continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HSMul.hSMul (β := A) s
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
⊢ cfcₙ (p := p) (fun (x : R) ↦ s • f x) a = s • cfcₙ (p := p) f a

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply _ a]

Premises used: cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
S : Type u_3
inst_12 : SMulZeroClass S R
inst_13 : ContinuousConstSMul S R
inst_14 : SMulZeroClass S A
inst_15 : IsScalarTower S R A
inst_16 : IsScalarTower S R (R → R)
s : S
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
pos :
  (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (HSMul.hSMul (β := R) s 1 • f), continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HSMul.hSMul (β := A) (HSMul.hSMul (β := R) s 1)
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
⊢ (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ s • f x, continuous_toFun := ⋯,
        map_zero' := ⋯ } =
    HSMul.hSMul (β := A) s
      ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)

Tactic:
simp_rw [← Pi.smul_def, ← smul_one_smul R s _]

Premises used: smul_one_smul, Pi.smul_def