-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_inv_id (a : Aˣ) (ha : p a

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
hx : 0 ∈ spectrum R ↑a
⊢ False

Tactic:
exact spectrum.zero_not_mem R a.isUnit hx

Result:
no goals

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ ∀ x ∈ spectrum R ↑a, id x ≠ 0

Tactic:
rintro x hx rfl

Result:
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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
hx : 0 ∈ spectrum R ↑a
⊢ False

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ cfc (fun x => x⁻¹) ↑a = Ring.inverse ↑a

Tactic:
convert cfc_inv (id : R → R) (a : A) ?_

Result:
case h.e'_3.h.e'_3
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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ ↑a = cfc id ↑a

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ ∀ x ∈ spectrum R ↑a, id x ≠ 0

Proof state:
case h.e'_3.h.e'_3
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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ ↑a = cfc id ↑a

Tactic:
exact (cfc_id R (a : A)).symm

Result:
no goals

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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ cfc (fun x => x⁻¹) ↑a = ↑a⁻¹

Tactic:
rw [← Ring.inverse_unit]

Result:
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✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : HasContinuousInv₀ R
a : Aˣ
ha : autoParam (p ↑a) _auto✝
⊢ cfc (fun x => x⁻¹) ↑a = Ring.inverse ↑a