-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
/-- When `cfc` is applied to a function that maps zero to zero, it is equivalent to using
`cfcₙ`. -/
lemma cfcₙ_eq_cfc [ContinuousMapZero.UniqueHom R A] {f : R → R} {a : A}
    (hf : ContinuousOn f (σₙ R a)

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
hf' : ContinuousOn f (spectrum R a)
⊢ ((↑(cfcHom ha)).comp
        ((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom))
      { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

Tactic:
dsimp only [NonUnitalStarAlgHom.comp_apply, toContinuousMapHom_apply,
  NonUnitalStarAlgHom.coe_coe, compStarAlgHom'_apply]

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
hf' : ContinuousOn f (spectrum R a)
⊢ (cfcHom ha)
      ((↑{ toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }).comp
        { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) =
    (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
hf' : ContinuousOn f (spectrum R a)
⊢ cfcₙ f a = cfc f a

Tactic:
rw [cfc_apply f a ha hf', cfcₙ_apply f a hf, cfcₙHom_eq_cfcₙHom_of_cfcHom, cfcₙHom_of_cfcHom]

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
hf' : ContinuousOn f (spectrum R a)
⊢ ((↑(cfcHom ha)).comp
        ((↑(compStarAlgHom' R R { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })).comp toContinuousMapHom))
      { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
⊢ cfcₙ f a = cfc f a

Tactic:
by_cases ha : p a

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
⊢ cfcₙ f a = cfc f a

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : ¬p a
⊢ cfcₙ f a = cfc f a

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
⊢ cfcₙ f a = cfc f a

Tactic:
have hf' := hf.mono <| spectrum_subset_quasispectrum R a

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
hf' : ContinuousOn f (spectrum R a)
⊢ cfcₙ f a = cfc f a

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : ¬p a
⊢ cfcₙ f a = cfc f a

Tactic:
simp [cfc_apply_of_not_predicate a ha, cfcₙ_apply_of_not_predicate (R := R) a ha]

Result:
no goals

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra R A
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMapZero.UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : p a
hf' : ContinuousOn f (spectrum R a)
⊢ (cfcHom ha)
      ((↑{ toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }).comp
        { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }) =
    (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

Tactic:
congr

Result:
no goals