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

Proof state:
case negSucc
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✝
n : ℕ
this : cfc (fun x => x⁻¹ ^ (n + 1)) ↑a = cfc (fun x => x⁻¹) ↑a ^ (n + 1)
⊢ cfc (fun x => x⁻¹ ^ (n + 1)) ↑a = ↑a⁻¹ ^ (n + 1)

Tactic:
exact this.trans <| congr($(cfc_inv_id a) ^ (n + 1))

Result:
no goals

Proof state:
case negSucc
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✝
n : ℕ
⊢ cfc (fun x => x ^ Int.negSucc n) ↑a = ↑(a ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, ← inv_pow, Units.val_pow_eq_pow_val]

Result:
case negSucc
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✝
n : ℕ
⊢ cfc (fun x => x⁻¹ ^ (n + 1)) ↑a = ↑a⁻¹ ^ (n + 1)

Proof state:
case negSucc
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✝
n : ℕ
⊢ cfc (fun x => x⁻¹ ^ (n + 1)) ↑a = ↑a⁻¹ ^ (n + 1)

Tactic:
have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)

Result:
case negSucc
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✝
n : ℕ
this : cfc (fun x => x⁻¹ ^ (n + 1)) ↑a = cfc (fun x => x⁻¹) ↑a ^ (n + 1)
⊢ cfc (fun x => x⁻¹ ^ (n + 1)) ↑a = ↑a⁻¹ ^ (n + 1)

Proof state:
case ofNat
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✝
n : ℕ
⊢ cfc (fun x => x ^ Int.ofNat n) ↑a = ↑(a ^ Int.ofNat n)

Tactic:
simpa using cfc_pow_id (a : A) n

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ˣ
n : ℤ
ha : autoParam (p ↑a) _auto✝
⊢ cfc (fun x => x ^ n) ↑a = ↑(a ^ n)

Tactic:
cases n with
| ofNat n => simpa using cfc_pow_id (a : A) n
| negSucc n =>
  simp only [zpow_negSucc, ← inv_pow, Units.val_pow_eq_pow_val]
  have := cfc_pow (fun x ↦ x⁻¹ : R → R) (n + 1) (a : A)
  exact this.trans <| congr($(cfc_inv_id a) ^ (n + 1))

Result:
no goals