-- 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 neg
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) := not_and_or.mp h

Result:
case neg.inl
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)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

case neg.inr
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)
ha : ¬p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Proof state:
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✝
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
by_cases h : ContinuousOn f (σₙ R a) ∧ p a

Result:
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

case neg
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

Proof state:
case neg.inr
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)
ha : ¬p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
  cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]

Result:
no goals

Proof state:
case neg.inl
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)
hf : ¬ContinuousOn f (σₙ R a)
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero,
  cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)]

Result:
no goals

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:
exact (inrNonUnitalStarAlgHom ℂ A).map_cfcₙ f a

Result:
no goals