-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
/-- This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke
versions for `ℝ≥0`, `ℝ`, and `ℂ`. -/
lemma Unitization.cfcₙ_eq_cfc_inr {R : Type*} [Semifield R] [StarRing R] [MetricSpace R]
    [IsTopologicalSemiring R] [ContinuousStar R] [Module R A] [IsScalarTower R A A]
    [SMulCommClass R A A] [CompleteSpace R] [Algebra R ℂ] [IsScalarTower R ℂ A]
    {p : A → Prop} {p' : A⁺¹ → Prop} [NonUnitalContinuousFunctionalCalculus R p]
    [ContinuousFunctionalCalculus R p']
    [ContinuousMapZero.UniqueHom R (Unitization ℂ A)]
    (hp : ∀ {a : A}, p' (a : A⁺¹) ↔ p a) (a : A) (f : R → R) (hf₀ : f 0 = 0

Proof state:
case pos
A : Type u_2
inst✝¹⁴ : NonUnitalCStarAlgebra A
R : Type u_3
inst✝¹³ : Semifield R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : CompleteSpace R
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R p
inst✝¹ : ContinuousFunctionalCalculus R p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : autoParam (f 0 = 0) _auto✝
h : ContinuousOn f (σₙ R a) ∧ p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
obtain ⟨hf, ha⟩ := h

Result:
case pos.intro
A : Type u_2
inst✝¹⁴ : NonUnitalCStarAlgebra A
R : Type u_3
inst✝¹³ : Semifield R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : CompleteSpace R
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R p
inst✝¹ : ContinuousFunctionalCalculus R p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : autoParam (f 0 = 0) _auto✝
hf : ContinuousOn f (σₙ R a)
ha : p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Proof state:
case pos.intro
A : Type u_2
inst✝¹⁴ : NonUnitalCStarAlgebra A
R : Type u_3
inst✝¹³ : Semifield R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : CompleteSpace R
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R p
inst✝¹ : ContinuousFunctionalCalculus R p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : autoParam (f 0 = 0) _auto✝
hf : ContinuousOn f (σₙ R a)
ha : p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
rw [← cfcₙ_eq_cfc (quasispectrum_inr_eq R ℂ a ▸ hf)]

Result:
case pos.intro
A : Type u_2
inst✝¹⁴ : NonUnitalCStarAlgebra A
R : Type u_3
inst✝¹³ : Semifield R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : CompleteSpace R
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R p
inst✝¹ : ContinuousFunctionalCalculus R p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : autoParam (f 0 = 0) _auto✝
hf : ContinuousOn f (σₙ R a)
ha : p a
⊢ ↑(cfcₙ f a) = cfcₙ f ↑a