awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
h₁ : x ^ p = x * x ^ (p - 1)
rw :
  x *
      HMul.hMul (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
            (p - 1).rpowIntegrand₀₁ t 1)⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t x) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
      (x *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ x_1 x)
⊢ x ^ p =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
      (x *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ x_1 x)

Tactic:
rw [h₁, rpow_eq_const_mul_integral (by grind) hx]

Premises used: Real.rpow_eq_const_mul_integral
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p x : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
hx : 0 ≤ x
hmain :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x) fun (x_1 : ℝ) ↦ x * (p - 1).rpowIntegrand₀₁ x_1 x
h₁ : x ^ p = x * x ^ (p - 1)
⊢ x *
      HMul.hMul (α := ℝ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
            (p - 1).rpowIntegrand₀₁ t 1)⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t x) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ t 1)⁻¹ *
      (x *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x_1 : ℝ) ↦
          (p - 1).rpowIntegrand₀₁ x_1 x)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
rw :
  LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (p - 1).rpowIntegrand₀₁ t 1)
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹

Tactic:
rw [inv_nonneg]

Premises used: inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
⊢ Membership.mem (γ := Set ℝ) (Ioo 0 1) (p - 1)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (p - 1).rpowIntegrand₀₁ t 1)

Tactic:
exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos (by grind)

Premises used: le_of_lt, Real.integral_rpowIntegrand₀₁_one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
⊢ ∃ (μ : Measure ℝ),
    ∀ (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 ∂μ

Tactic:
⟨μ, fun x hx => ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
    IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ
refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x), x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ
⊢ ∃ (μ : Measure ℝ),
    ∀ (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 ∂μ

Tactic:
refine ⟨μ, fun x hx => ⟨?_, ?_⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_1 :
  Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) ((HSMul.hSMul (β := Measure ℝ) C volume).restrict (Ioi 0))
⊢ IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) (Ioi 0) μ

Tactic:
unfold μ IntegrableOn

Premises used: MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_1 :
  Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x)
    (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x) ((HSMul.hSMul (β := Measure ℝ) C volume).restrict (Ioi 0))

Tactic:
rw [Measure.restrict_smul]

Premises used: MeasureTheory.Measure.restrict_smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x)
    (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))

Tactic:
Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₁₂ hp hx

Premises used: MeasureTheory.Integrable.smul_measure_nnreal, Real.integrableOn_rpowIntegrand₁₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Integrable (ε := ℝ) (fun (t : ℝ) ↦ p.rpowIntegrand₁₂ t x)
    (HSMul.hSMul (β := Measure ℝ) C (Measure.restrict volume (Ioi 0)))

Tactic:
exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₁₂ hp hx

Premises used: MeasureTheory.Integrable.smul_measure_nnreal, Real.integrableOn_rpowIntegrand₁₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
refine_2 :
  HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).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 (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x)
⊢ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₁₂ t x ∂μ

Tactic:
rw [Measure.restrict_smul, integral_smul_nnreal_measure,
      rpow_eq_const_mul_integral_rpowIntegrand₁₂ hp hx]

Premises used: MeasureTheory.Measure.restrict_smul, MeasureTheory.integral_smul_nnreal_measure, Real.rpow_eq_const_mul_integral_rpowIntegrand₁₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Goal:
p : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 1 2) p
C : ℝ≥0 :=
  NNReal.mk
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (p - 1).rpowIntegrand₀₁ t 1)⁻¹
    ⋯
μ : Measure ℝ := HSMul.hSMul (β := Measure ℝ) C volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          (p - 1).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 (x_1 : ℝ) ↦ p.rpowIntegrand₁₂ x_1 x)

Tactic:
simp [C, NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
⊢ quasispectrum ℝ a ⊆ Ici 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
⊢ quasispectrum ℝ a ⊆ Ici 0

Tactic:
have hspec : quasispectrum ℝ a ⊆ Ici 0 := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ 0 ≤ x

Tactic:
simp only [mem_Ici, smul_eq_mul] at hx ⊢

Premises used: Set.mem_Ici, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ t⁻¹ * x

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
⊢ MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)

Tactic:
have h_mapsTo : MapsTo (t⁻¹ • · : ℝ → ℝ) (Ici 0) (Ici 0) := by
    intro x hx
    simp only [mem_Ici, smul_eq_mul] at hx ⊢
    positivity
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
refine : EqOn (p.rpowIntegrand₀₁ t) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)
⊢ cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ t) a =
    cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
refine cfcₙ_congr ?_

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ EqOn (p.rpowIntegrand₀₁ t) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)

Tactic:
Set.EqOn.mono hspec (rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one ht)

Premises used: Set.EqOn.mono, Real.rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ EqOn (p.rpowIntegrand₀₁ t) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)

Tactic:
refine Set.EqOn.mono hspec (rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one ht)

Premises used: Set.EqOn.mono, Real.rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat, cfcₙ_smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
refine : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a

Tactic:
refine cfcₙ_smul (R := ℝ) (t ^ ((p : ℝ) - 1)) _ a ?_

Premises used: HSub.hSub, HPow.hPow, OfNat.ofNat, cfcₙ_smul
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)

Tactic:
ContinuousOn.mono ?_ hspec

Premises used: ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
refine : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (quasispectrum ℝ a)

Tactic:
refine ContinuousOn.mono ?_ hspec

Premises used: ContinuousOn.mono
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (p.rpowIntegrand₀₁ 1) (Ici 0)

Tactic:
have := continuousOn_rpowIntegrand₀₁_Ici hp zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
this : ContinuousOn (p.rpowIntegrand₀₁ 1) (Ici 0)
funProp : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
h :
  cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)
⊢ t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    t ^ (p - 1) • cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
congr! 1
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
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
p t : ℝ
hp : Membership.mem (γ := Set ℝ) (Ioo 0 1) p
ht : 0 < t
a : A
ha : 0 ≤ a
hspec : quasispectrum ℝ a ⊆ Ici 0
h_mapsTo : MapsTo (β := ℝ) (fun (x : ℝ) ↦ t⁻¹ • x) (Ici 0) (Ici 0)
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) a =
    cfcₙ (p := IsSelfAdjoint) (p.rpowIntegrand₀₁ 1) (t⁻¹ • a)

Tactic:
cfcₙ_comp_smul (R := ℝ) t⁻¹ (fun x => rpowIntegrand₀₁ p 1 x) a ?_

Premises used: Real.rpowIntegrand₀₁, cfcₙ_comp_smul, Inv.inv, OfNat.ofNat