-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_neg [IsTopologicalRing A] [T2Space A] (a : Aˣ) (x : ℝ)
    (ha' : (0 : A) ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
h₁ : ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 ↑a
⊢ x✝¹ ^ (-x) = x✝¹⁻¹ ^ x

Tactic:
simp [NNReal.rpow_neg, NNReal.inv_rpow]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
⊢ ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)

Tactic:
refine NNReal.continuousOn_rpow_const (.inl ?_)

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
⊢ 0 ∉ Inv.inv '' spectrum ℝ≥0 ↑a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
h₁ : ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)
⊢ ↑a ^ (-x) = ↑a⁻¹ ^ x

Tactic:
rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
    ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
h₁ : ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)
⊢ cfc (fun x_1 => x_1 ^ (-x)) ↑a = cfc (fun x_1 => x_1⁻¹ ^ x) ↑a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
h₁ : ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)
⊢ cfc (fun x_1 => x_1 ^ (-x)) ↑a = cfc (fun x_1 => x_1⁻¹ ^ x) ↑a

Tactic:
refine cfc_congr fun _ _ => ?_

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
h₁ : ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 ↑a
⊢ x✝¹ ^ (-x) = x✝¹⁻¹ ^ x

Proof state:
case intro.intro
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 ↑a
hz' : z⁻¹ = 0
⊢ False

Tactic:
exact spectrum.zero_not_mem ℝ≥0 a.isUnit <| inv_eq_zero.mp hz' ▸ hz

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ (-x) = ↑a⁻¹ ^ x

Tactic:
suffices h₁ : ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' (spectrum ℝ≥0 (a : A))) by
  rw [← cfc_inv_id (R := ℝ≥0) a, rpow_def, rpow_def,
      ← cfc_comp' (fun z => z ^ x) (Inv.inv : ℝ≥0 → ℝ≥0) (a : A) h₁]
  refine cfc_congr fun _ _ => ?_
  simp [NNReal.rpow_neg, NNReal.inv_rpow]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
⊢ ContinuousOn (fun z => z ^ x) (Inv.inv '' spectrum ℝ≥0 ↑a)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
⊢ 0 ∉ Inv.inv '' spectrum ℝ≥0 ↑a

Tactic:
rintro ⟨z, hz, hz'⟩

Result:
case intro.intro
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : Aˣ
x : ℝ
ha' : autoParam (0 ≤ ↑a) _auto✝
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 ↑a
hz' : z⁻¹ = 0
⊢ False