awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : SMulCommClass ℝ A A
inst_4 : IsScalarTower ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : CompleteSpace A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 1 2) p
μ : Measure ℝ
hμ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧
        x ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : Membership.mem (γ := Set ℝ) (Ioo 1 2) (↑p : ℝ)
f : (t x : ℝ) → ℝ := fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
a₁ : a ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ
have a₂ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a =
  cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a
Tactic: calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : SMulCommClass ℝ A A
inst_4 : IsScalarTower ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : CompleteSpace A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 1 2) p
μ : Measure ℝ
hμ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧
        x ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : Membership.mem (γ := Set ℝ) (Ioo 1 2) (↑p : ℝ)
f : (t x : ℝ) → ℝ := fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ
have case : a ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
Tactic: case integral => calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (goal)
Goal:
A : Type u_1
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : SMulCommClass ℝ A A
inst_4 : IsScalarTower ℝ A A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : CompleteSpace A
p : ℝ≥0
hp : Membership.mem (γ := Set ℝ≥0) (Ioo 1 2) p
μ : Measure ℝ
hμ :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ici 0) x →
      IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t x) (Ioi 0) μ ∧
        x ^ (↑p : ℝ) = ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t x ∂μ
a : A
ha : 0 ≤ a
hpcoe : Membership.mem (γ := Set ℝ) (Ioo 1 2) (↑p : ℝ)
f : (t x : ℝ) → ℝ := fun (t : ℝ) ↦ (↑p : ℝ).rpowIntegrand₁₂ t
maxr : ℝ := sSup (quasispectrum ℝ a)
maxr_nonneg : 0 ≤ maxr
bound : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ‖f t maxr‖
hf : ContinuousOn (Function.uncurry f) (SProd.sprod (α := Set ℝ) (Ioi 0) (quasispectrum ℝ a))
hbound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ioi 0), ∀ z ∈ quasispectrum ℝ a, ‖f t z‖ ≤ bound t
hbound_finite_integral : HasFiniteIntegral bound (μ.restrict (Ioi 0))
hmapzero : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioi 0), (↑p : ℝ).rpowIntegrand₁₂ x 0 = 0
case : a ^ p = cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a
⊢ a ^ p = ∫ (t : ℝ) in Ioi 0, cfcₙ (p := IsSelfAdjoint) ((↑p : ℝ).rpowIntegrand₁₂ t) a ∂μ
have case₁ : cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ x.nnrpow p) a =
  cfcₙ (p := IsSelfAdjoint) (fun (r : ℝ) ↦ ∫ (t : ℝ) in Ioi 0, (↑p : ℝ).rpowIntegrand₁₂ t r ∂μ) a
Tactic: case integral => calc
      a ^ p = cfcₙ (fun x => NNReal.nnrpow x p) a := by
        rw [CFC.nnrpow_def]
      _ = cfcₙ (fun r => ∫ t in Ioi 0, rpowIntegrand₁₂ p t r ∂μ) a := by
        rw [cfcₙ_nnreal_eq_real ..]
        refine cfcₙ_congr fun r hr => ?_
        have hr' : 0 ≤ r := by grind
        simp only [sup_of_le_left hr', NNReal.nnrpow_def, NNReal.coe_rpow, coe_toNNReal']
        exact (hμ r hr').2
      _ = ∫ t in Ioi 0, cfcₙ (rpowIntegrand₁₂ p t) a ∂μ :=
        cfcₙ_setIntegral measurableSet_Ioi _ bound a hf hmapzero hbound
          hbound_finite_integral ha.isSelfAdjoint
-- 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
⊢ cfc (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 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
have rw : 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
Tactic: rw [rpowIntegrand₀₁_eq_sub (by grind) ht]
-- 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
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
have funProp : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
Tactic: fun_prop (disch := grind -abstractProof)
-- 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
funProp : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
have funProp₁ : ∀ (x : ℝ), x ≠ 0
Tactic: fun_prop (disch := grind -abstractProof)
-- 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
funProp : ∀ x ∈ spectrum ℝ (↑?a : ?A), x ≠ 0
funProp₁ : ∀ (x : ℝ), x ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
have funProp₂ : ∀ x_1 ∈ spectrum ℝ x, t + x_1 ≠ 0
Tactic: fun_prop (disch := grind -abstractProof)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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
⊢ 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 hg : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ (t + z)⁻¹) (spectrum ℝ x)
Tactic: have hg : ContinuousOn (fun z : ℝ => (t + z)⁻¹) (spectrum ℝ x) := by
      fun_prop (disch := grind -abstractProof)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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)
⊢ 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 hf : ContinuousOn (Y := ℝ) (fun (z : ℝ) ↦ 1 + z) (spectrum ℝ x)
Tactic: have hf : ContinuousOn (fun z : ℝ => (1 + z)) (spectrum ℝ x) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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)
⊢ 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 hspectrum : ∀ r ∈ spectrum ℝ x, t + r ≠ 0
Tactic: have hspectrum :  ∀ r ∈ spectrum ℝ x, t + r ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation (hypothesis)
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
⊢ 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 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
Tactic: have := cfc_sub (fun _ : ℝ => t ^ (p - 1)) (fun z : ℝ => t ^ p * (t + z)⁻¹) x
-- 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
⊢ 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 : 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
Tactic: rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]
-- 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
⊢ 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)
    (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
Tactic: rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]
-- 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
⊢ 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 • 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
Tactic: rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]
-- 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
⊢ 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 (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
Tactic: rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]
-- 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
⊢ 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) (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
Tactic: rw [this, cfc_const .., cfc_const_mul .., cfc_inv _ _ hspectrum .., cfc_const_add ..,
        cfc_id' ..]