Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : f 0 = 0
⊢ cfcₙ f a = fun i ↦ cfcₙ f (a i)

pp: case neg
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : ¬f 0 = 0
⊢ cfcₙ f a = fun i ↦ cfcₙ f (a i)

Tactic:
· ext i
    have : Nonempty ι := ⟨i⟩
    let φ := Pi.evalNonUnitalStarAlgHom S A i
    exact φ.map_cfcₙ f a (by rwa [Pi.quasispectrum_eq]) hf₀ (continuous_apply i) ha (ha' i)

Goal state after:
case neg
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : ¬f 0 = 0
⊢ cfcₙ f a = fun i ↦ cfcₙ f (a i)