-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_add {a : A} {x y : ℝ} (ha : 0 ∉ spectrum ℝ≥0 a) :
    a ^ (x + y) = a ^ x * a ^ y

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
this : z ≠ 0
⊢ (fun x_1 => x_1 ^ (x + y)) z = (fun x_1 => x_1 ^ x * x_1 ^ y) z

Tactic:
simp [NNReal.rpow_add this _ _]

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (fun x_1 => x_1 ^ (x + y)) a = cfc (fun x_1 => x_1 ^ x * x_1 ^ y) a

Tactic:
refine cfc_congr ?_

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ Set.EqOn (fun x_1 => x_1 ^ (x + y)) (fun x_1 => x_1 ^ x * x_1 ^ y) (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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ a ^ (x + y) = a ^ x * a ^ y

Tactic:
simp only [rpow_def, NNReal.rpow_eq_pow]

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (fun x_1 => x_1 ^ (x + y)) a = cfc (fun x_1 => x_1 ^ x) a * cfc (fun x => x ^ y) 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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ Set.EqOn (fun x_1 => x_1 ^ (x + y)) (fun x_1 => x_1 ^ x * x_1 ^ y) (spectrum ℝ≥0 a)

Tactic:
intro z hz

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
⊢ (fun x_1 => x_1 ^ (x + y)) z = (fun x_1 => x_1 ^ x * x_1 ^ y) z

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
⊢ z ≠ 0

Tactic:
aesop

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (fun x_1 => x_1 ^ (x + y)) a = cfc (fun x_1 => x_1 ^ x) a * cfc (fun x => x ^ y) a

Tactic:
rw [← cfc_mul _ _ a]

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
⊢ cfc (fun x_1 => x_1 ^ (x + y)) a = cfc (fun x_1 => x_1 ^ x * x_1 ^ y) 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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
⊢ (fun x_1 => x_1 ^ (x + y)) z = (fun x_1 => x_1 ^ x * x_1 ^ y) z

Tactic:
have : z ≠ 0 := by aesop

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
a : A
x y : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
z : ℝ≥0
hz : z ∈ spectrum ℝ≥0 a
this : z ≠ 0
⊢ (fun x_1 => x_1 ^ (x + y)) z = (fun x_1 => x_1 ^ x * x_1 ^ y) z