-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
A : Type u_1
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
x : A
hx : Membership.mem (γ := Set A) (Ici 0) x
hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
hf : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)
hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
this :
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1)) x -
      cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ t ^ p * (t + z)⁻¹) x
rw :
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1)) x -
      cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ t ^ p * (t + z)⁻¹) x =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
rw₁ :
  HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ t ^ p * (t + z)⁻¹) x) =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
rw₂ :
  HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (t ^ p • cfc (p := IsSelfAdjoint) (fun (z : ℝ) ↦ (t + z)⁻¹) x) =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
rw₃ :
  HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (t ^ p • Ring.inverse (cfc (p := IsSelfAdjoint) (HAdd.hAdd t) x)) =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
rw₄ :
  HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
      (t ^ p •
        Ring.inverse
          (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) (cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x) x))) =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun (x : A) ↦
        HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
          (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
      x
have rw₅ : HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
    (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)) =
  (fun (x : A) ↦
      HSub.hSub (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (t ^ (p - 1)) : A)
        (t ^ p • Ring.inverse (HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) t : A) x)))
    x
Tactic: rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]