-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t 1)⁻¹
    ⋯
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_2 : x ^ p = ∫ (t : ℝ), p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0))
refine_2₁ :
  x ^ p =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₂ :
  HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x) =
    HSMul.hSMul (β := ℝ) C
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₃ :
  HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x) =
    HSMul.hSMul (β := ℝ) (↑C : ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₄ :
  HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x) =
    HSMul.hSMul (β := ℝ)
      (↑(NNReal.mk
            (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
                p.rpowIntegrand₀₁ t 1)⁻¹
            ⋯) :
        ℝ)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
refine_2₅ :
  HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        p.rpowIntegrand₀₁ t x) =
    HSMul.hSMul (α := ℝ) (β := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          p.rpowIntegrand₀₁ t 1)⁻¹
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦ p.rpowIntegrand₀₁ t x)
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂HSMul.hSMul (β := Measure ℝ) C volume

Tactic:
simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]

Premises used: MeasureTheory.Measure.restrict_smul, MeasureTheory.integral_smul_nnreal_measure, Real.rpow_eq_const_mul_integral, NNReal.coe_mk, NNReal.smul_def, smul_eq_mul