awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
rw :
  ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1))) =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))

Tactic:
rw [lintegral_rpow_eq_lintegral_meas_le_mul μ f_nn f_mble p_pos]

Premises used: MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
apply :
  ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
        (ENNReal.ofReal (t ^ (p - 1))) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
⊢ ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1))) =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))

Tactic:
apply congr_arg fun z => ENNReal.ofReal p * z

Premises used: HMul.hMul, ENNReal.ofReal, congr_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
h :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ENNReal)
    (fun (a : ℝ) ↦
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a ≤ f a_1} : ENNReal)
        (ENNReal.ofReal (a ^ (p - 1))))
    fun (a : ℝ) ↦
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a < f a_1} : ENNReal)
      (ENNReal.ofReal (a ^ (p - 1)))
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
        (ENNReal.ofReal (t ^ (p - 1))) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
h :
  ∀ (t : ℝ)
    (ht :
      Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
        ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)),
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ENNReal)
    (fun (a : ℝ) ↦
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a ≤ f a_1} : ENNReal)
        (ENNReal.ofReal (a ^ (p - 1))))
    fun (a : ℝ) ↦
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a < f a_1} : ENNReal)
      (ENNReal.ofReal (a ^ (p - 1)))

Tactic:
filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht

Premises used: Set.Ioi, MeasureTheory.meas_le_ae_eq_meas_lt, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
t : ℝ
ht :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
    ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
h h₁ :
  HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
⊢ HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))

Tactic:
rw [ht]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
apply : 0 < Module.finrank ℝ E
⊢ Nontrivial E

Tactic:
apply Module.nontrivial_of_finrank_pos (R := ℝ)

Premises used: Module.nontrivial_of_finrank_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ 0 < Module.finrank ℝ E

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ Nontrivial E

Tactic:
haveI : Nontrivial E := by
    apply Module.nontrivial_of_finrank_pos (R := ℝ)
    positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
pos :
  ∀ (hr : 0 < r),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
neg :
  ∀ (hr : r ≤ 0),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
      (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume

Tactic:
by_cases! hr : 0 < r
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hr : 0 < r
pos : -1 < HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume

Tactic:
rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]

Premises used: intervalIntegral.integrableOn_Ioo_rpow_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hr : 0 < r
linarith :
  HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α ≤ -1 →
    α - (↑(Module.finrank ℝ E) : ℝ) + (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α - -1) = 0
⊢ -1 < HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hr : r ≤ 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume

Tactic:
have h_rpow : IntegrableOn (fun y ↦ y ^ ((Module.finrank ℝ E : ℝ) - 1 - α)) (Ioo 0 r) := by
      by_cases! hr : 0 < r
      · rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith
      · simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
apply :
  EqOn (β := ℝ) (fun (x : ℝ) ↦ C * x ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α))
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r) volume

Tactic:
apply IntegrableOn.congr_fun (h_rpow.const_mul C) ?_ measurableSet_Ioo

Premises used: MeasureTheory.Integrable.const_mul, measurableSet_Ioo, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
this₁ :
  ∀ (hy : 0 < y),
    y < r →
      Eq (α := ℝ) ((fun (x : ℝ) ↦ C * x ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) y)
        ((fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) y)
⊢ y ∈ Ioo 0 r →
    Eq (α := ℝ) ((fun (x : ℝ) ↦ C * x ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) y)
      ((fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) y)

Tactic:
⟨hy, _⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
move_mul : y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ (Module.finrank ℝ E - 1) * y ^ (-α) * C
⊢ C * y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) = y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))

Tactic:
move_mul [C]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
rw : y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ ((↑(Module.finrank ℝ E - 1) : ℝ) + -α) * C
⊢ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ (Module.finrank ℝ E - 1) * y ^ (-α) * C

Tactic:
rw [← Real.rpow_natCast y (Module.finrank ℝ E - 1), ← Real.rpow_add hy]

Premises used: Real, HSub.hSub, Real.rpow_add, OfNat.ofNat, Module.finrank, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
e_a : HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 = (↑(Module.finrank ℝ E - 1) : ℝ)
⊢ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α) * C = y ^ ((↑(Module.finrank ℝ E - 1) : ℝ) + -α) * C

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right : y < r
e_a e_a₁ e_a₂ e_a₃ : Module.finrank ℝ E - 1 = Module.finrank ℝ E - 1
⊢ HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 = (↑(Module.finrank ℝ E - 1) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) volume

Tactic:
have hint : IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) := by
    simp only [smul_eq_mul]
    have h_rpow : IntegrableOn (fun y ↦ y ^ ((Module.finrank ℝ E : ℝ) - 1 - α)) (Ioo 0 r) := by
      by_cases! hr : 0 < r
      · rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith
      · simp [hr]
    apply IntegrableOn.congr_fun (h_rpow.const_mul C) ?_ measurableSet_Ioo
    intro y ⟨hy, _⟩
    simp only
    move_mul [C]
    rw [← Real.rpow_natCast y (Module.finrank ℝ E - 1), ← Real.rpow_add hy]
    congr
    norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (Module.finrank ℝ E - 1) • (C * y ^ (-α))) (Ioo 0 r) volume
⊢ IntegrableOn (ε := ℝ) (fun (x : E) ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ

Tactic:
rw [← integrableOn_fun_norm_addHaar μ] at hint

Premises used: MeasureTheory.integrableOn_fun_norm_addHaar
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (ε := ℝ) (fun (x : E) ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
⊢ IntegrableOn f (ball 0 r) μ

Tactic:
Integrable.mono' hint h_meas.restrict h_decay

Premises used: MeasureTheory.Integrable.mono', MeasureTheory.IntegrableOn, MeasureTheory.AEStronglyMeasurable.restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (ε := ℝ) (fun (x : E) ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
⊢ IntegrableOn f (ball 0 r) μ

Tactic:
exact Integrable.mono' hint h_meas.restrict h_decay

Premises used: MeasureTheory.Integrable.mono', MeasureTheory.AEStronglyMeasurable.restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
rw : ∀ (k : Set E), IsCompact k → IntegrableOn f k μ
⊢ LocallyIntegrable f μ

Tactic:
rw [locallyIntegrable_iff]

Premises used: MeasureTheory.locallyIntegrable_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
K : Set E
hK : IsCompact K
obtain : ∀ (R : ℝ) (hR_pos : R > 0) (hR : ∀ x ∈ K, ‖x‖ < R), IntegrableOn f K μ
⊢ IntegrableOn f K μ

Tactic:
obtain ⟨R, hR_pos, hR⟩ := hK.isBounded.exists_pos_norm_lt

Premises used: IsCompact.isBounded, Bornology.IsBounded.exists_pos_norm_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
K : Set E
hK : IsCompact K
R : ℝ
hR_pos : R > 0
hR : ∀ x ∈ K, ‖x‖ < R
⊢ IntegrableOn f K μ

Tactic:
(integrableOn_ball_of_norm_le_rpow hdim hα (ae_restrict_of_ae h_decay) h_meas).mono_set
    (mem_ball_zero_iff.mpr <| hR · ·)

Premises used: Iff.mpr, MeasureTheory.integrableOn_ball_of_norm_le_rpow, MeasureTheory.ae_restrict_of_ae, MeasureTheory.IntegrableOn.mono_set, mem_ball_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hdim : 1 ≤ Module.finrank ℝ E
f : E → F
C α : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ, ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
K : Set E
hK : IsCompact K
R : ℝ
hR_pos : R > 0
hR : ∀ x ∈ K, ‖x‖ < R
⊢ IntegrableOn f K μ

Tactic:
exact (integrableOn_ball_of_norm_le_rpow hdim hα (ae_restrict_of_ae h_decay) h_meas).mono_set
    (mem_ball_zero_iff.mpr <| hR · ·)

Premises used: Iff.mpr, MeasureTheory.integrableOn_ball_of_norm_le_rpow, MeasureTheory.ae_restrict_of_ae, MeasureTheory.IntegrableOn.mono_set, mem_ball_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
a : ℕ
⊢ nthRoot 0 a = 1

Tactic:
rfl

Premises used: Nat.nthRoot, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
⊢ nthRoot 1 = id

Tactic:
rfl

Premises used: Nat.nthRoot, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Goal:
n : ℕ
h : n ≠ 0
zero : ∀ (h : Ne (α := ℕ) 0 0), nthRoot 0 0 = 0
succ : ∀ (h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), (HAdd.hAdd (α := ℕ) 0 1).nthRoot 0 = 0
succ₁ : ∀ (n : ℕ) (h : n + 1 + 1 ≠ 0), (n + 1 + 1).nthRoot 0 = 0
⊢ n.nthRoot 0 = 0

Tactic:
rcases n with _ | _ | _