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
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
⊢ Continuous (X :=
    C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
        Type u_1),
      R)₀)
    (Y := C((↑(σₙ R a) : Type u_1), R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R)₀) _root_.toContinuousMap
      (⇑(↑ψ.toNonUnitalAlgHom :
            C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀ →ₙ*
              C((↑(σₙ R a) : Type u_1), R)₀) :
        (a_1 : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) →
          C((↑(σₙ R a) : Type u_1), R)₀))

Tactic:
f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom

Premises used: Continuous.comp, ContinuousMap.comp, ContinuousMapZero.toContinuousMap, toContinuousMap, continuous_induced_dom, ContinuousMap.continuous_precomp
-- 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
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
⊢ Continuous (X :=
    C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
        Type u_1),
      R)₀)
    (Y := C((↑(σₙ R a) : Type u_1), R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R)₀) _root_.toContinuousMap
      (⇑(↑ψ.toNonUnitalAlgHom :
            C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀ →ₙ*
              C((↑(σₙ R a) : Type u_1), R)₀) :
        (a_1 : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) →
          C((↑(σₙ R a) : Type u_1), R)₀))

Tactic:
exact f'.toContinuousMap.continuous_precomp.comp continuous_induced_dom

Premises used: Continuous.comp, ContinuousMapZero.toContinuousMap, continuous_induced_dom, ContinuousMap.continuous_precomp
-- 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
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
refine_2 :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (comp
          (ContinuousMapZero.id
            (quasispectrum.{u_1, u_2} R (A := A)
              ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)))
          f') :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1), R)₀) → A)
        (ContinuousMapZero.id
            (quasispectrum.{u_1, u_2} R (A := A)
              ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)

Tactic:
simp only [φ, ψ, NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_mk',
      NonUnitalAlgHom.coe_mk]

Premises used: NonUnitalStarAlgHom.comp_apply, NonUnitalAlgHom.coe_mk, NonUnitalStarAlgHom.coe_mk'
-- 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
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
refine_2 :
  comp
      (ContinuousMapZero.id
        (quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)))
      f' =
    f
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (comp
          (ContinuousMapZero.id
            (quasispectrum.{u_1, u_2} R (A := A)
              ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)))
          f') :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : 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
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
refine_2 :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R)
      ((comp
              (ContinuousMapZero.id
                (quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)))
              f' :
            (a : (↑(σₙ R a) : Type u_1)) → R)
          x :
        R)
      ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
⊢ comp
      (ContinuousMapZero.id
        (quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)))
      f' =
    f

Tactic:
ext x
-- 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
a : A
ha : p a
inst_12 : UniqueHom R A
f : C((↑(σₙ R a) : Type u_1), R)₀
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1))₀
hff' :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      ((↑((f' :
                (a_1 : (↑(σₙ R a) : Type u_1)) →
                  (↑(σₙ R ((cfcₙHom ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f)) : Type u_1))
              x) :
          R) :
        R)
g :
  C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀
ψ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  C((↑(σₙ R a) : Type u_1), R)₀ :=
  {
    toFun :=
      fun
        (x :
          C((↑(quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
              Type u_1),
            R)₀) ↦
      x.comp f',
    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C((↑(quasispectrum.{u_1, u_2} R (A := A) ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)) :
      Type u_1),
    R)₀ →⋆ₙₐ[R]
  A :=
  NonUnitalStarAlgHom.comp (cfcₙHom (p := p) ha) ψ
x : (↑(σₙ R a) : Type u_1)
⊢ Eq (α := R)
    ((comp
            (ContinuousMapZero.id
              (quasispectrum.{u_1, u_2} R (A := A)
                ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A)))
            f' :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
simp [hff']
-- 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 : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
        (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
      else 0 :
      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' := hf0 } :
      A)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
      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' := hf0 } :
      A)
⊢ cfcₙ (p := p) f 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' := hf0 }

Tactic:
rw [cfcₙ_def, dif_pos ⟨ha, hf, hf0⟩]

Premises used: cfcₙ_def, dif_pos
-- 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
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
h :
  ∀ (i : ι),
    cfcₙ (p := p) (f i) a =
      (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Eq (α := (i : ι) → A) (fun (i : ι) ↦ cfcₙ (p := p) (f i) a) fun (i : ι) ↦
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
ext i
-- 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
ha : p a
hf : ∀ (i : ι), ContinuousOn (f i) (σₙ R a)
hf0 : ∀ (i : ι), f i 0 = 0
i : ι
⊢ cfcₙ (p := p) (f i) a =
    (cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
simp only [cfcₙ_apply (f i) a (hf i) (hf0 i)]

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 : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) f a = 0

Tactic:
rw [cfcₙ_def, dif_neg ha]

Premises used: cfcₙ_def, dif_neg
-- 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 : R → R
a : A
ha : ¬p a
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_left _ ha)]

Premises used: cfcₙ_def, not_and_of_not_left, dif_neg
-- 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 : R → R
a : A
hf : ¬ContinuousOn f (σₙ R a)
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_left _ hf))]

Premises used: cfcₙ_def, not_and_of_not_left, dif_neg, not_and_of_not_right
-- 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 : R → R
a : A
hf : ¬f 0 = 0
rw :
  Eq.{u_2 + 1} (α := A)
    (if h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0 then
      (cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }
    else 0)
    0
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) f a = 0

Tactic:
rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_right _ hf))]

Premises used: cfcₙ_def, dif_neg, not_and_of_not_right