awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 • (|p_1.1| ^ q * rexp (-|p_1.1| ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 •
        (‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ q * rexp (-‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))

Tactic:
simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]

Premises used: Complex.norm_polarCoord_symm, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (x : ℝ) ↦ 1)

Tactic:
rw [← setIntegral_prod_mul, volume_eq_prod]

Premises used: MeasureTheory.setIntegral_prod_mul, MeasureTheory.Measure.volume_eq_prod
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-|z.1| ^ p))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1)

Tactic:
simp_rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
h : ∀ (x : ℝ × ℝ), x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) = x.1 * |x.1| ^ q * rexp (-|x.1| ^ p)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-|z.1| ^ p))

Tactic:
congr! 2
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ × ℝ
⊢ x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) = x.1 * |x.1| ^ q * rexp (-|x.1| ^ p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
linarith : π < -π → π - -π + 2 * (0 - π) = 0
linarith₁ : π < -π → GT.gt (α := ℝ) 2 0
⊢ -π ≤ π

Tactic:
linarith [pi_nonneg]

Premises used: Real.pi_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
e_a :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-|x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-x ^ p))
⊢ (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-x ^ p)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-|x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-x ^ p))

Tactic:
setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
e_a :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-|x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-x ^ p))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
rw [mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
e_a : x * x ^ q * rexp (-x ^ p) = x ^ q * x * rexp (-x ^ p)
⊢ x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)

Tactic:
rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]

Premises used: Iff.mpr, LT.lt.le, Real.rpow_one, Real.rpow_add, abs_eq_self
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-x ^ p) = x ^ q * x * rexp (-x ^ p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
⊢ 0 < p

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
linarith : q + 1 ≤ -1 → -2 - q + (q + 1 - -1) = 0
⊢ -1 < q + 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
rw : 2 * π * (1 / p * Real.Gamma ((q + 2) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)
⊢ (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-x ^ p)) =
    2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc,
        one_add_one_eq_two]

Premises used: integral_rpow_mul_exp_neg_rpow, add_assoc, one_add_one_eq_two
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + 2) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 •
        (‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ q *
          rexp (-b * ‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))

Tactic:
rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]

Premises used: Complex.integral_comp_polarCoord_symm, polarCoord_target
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 • (|p_1.1| ^ q * rexp (-b * |p_1.1| ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 •
        (‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ q *
          rexp (-b * ‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))

Tactic:
simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]

Premises used: Complex.norm_polarCoord_symm, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (x : ℝ) ↦ 1)

Tactic:
rw [← setIntegral_prod_mul, volume_eq_prod]

Premises used: MeasureTheory.setIntegral_prod_mul, MeasureTheory.Measure.volume_eq_prod
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1)

Tactic:
simp_rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
h : ∀ (x : ℝ × ℝ), x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) = x.1 * |x.1| ^ q * rexp (-b * |x.1| ^ p)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p))

Tactic:
congr! 2
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ × ℝ
⊢ x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) = x.1 * |x.1| ^ q * rexp (-b * |x.1| ^ p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
linarith : π < -π → π - -π + 2 * (0 - π) = 0
linarith₁ : π < -π → GT.gt (α := ℝ) 2 0
⊢ -π ≤ π

Tactic:
linarith [pi_nonneg]

Premises used: Real.pi_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
e_a :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-b * x ^ p))
⊢ (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-b * x ^ p))

Tactic:
setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
e_a :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-b * x ^ p))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
rw [mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
e_a : x * x ^ q * rexp (-b * x ^ p) = x ^ q * x * rexp (-b * x ^ p)
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]

Premises used: Iff.mpr, LT.lt.le, Real.rpow_one, Real.rpow_add, abs_eq_self
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ q * x * rexp (-b * x ^ p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
⊢ 0 < p

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
linarith : q + 1 ≤ -1 → -2 - q + (q + 1 - -1) = 0
⊢ -1 < q + 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
rw :
  2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
⊢ (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-b * x ^ p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc,
        one_add_one_eq_two]

Premises used: add_assoc, integral_rpow_mul_exp_neg_mul_rpow, one_add_one_eq_two
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 1 ≤ p
linarith : LE.le (α := ℝ) 0 (-2) → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (-2) = 0
linarith₁ : LE.le (α := ℝ) 0 (-2) → GT.gt (α := ℝ) 2 0
⊢ LT.lt (α := ℝ) (-2) 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 1 ≤ p
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-‖x‖ ^ p))
h₁ : π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p)) = π * Real.Gamma (2 / p + 1)

Tactic:
convert! (integral_rpow_mul_exp_neg_rpow hp (by linarith : (-2 : ℝ) < 0)) using 1

Premises used: Complex.integral_rpow_mul_exp_neg_rpow
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 1 ≤ p
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ 1 * rexp (-‖x‖ ^ p))
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-‖x‖ ^ p))

Tactic:
simp_rw [rpow_zero, one_mul]

Premises used: Real.rpow_zero, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 1 ≤ p
linarith : p = 0 → -1 + (1 - p) + (p - 0) = 0
⊢ p ≠ 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 1 ≤ p
h : π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)
⊢ π * Real.Gamma (2 / p + 1) = 2 * π / p * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)

Tactic:
rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]

Premises used: Real.Gamma_add_one, zero_add, div_ne_zero, two_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p : ℝ
hp : 1 ≤ p
⊢ π * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * Real.Gamma (2 / p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
linarith : LE.le (α := ℝ) 0 (-2) → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (-2) = 0
linarith₁ : LE.le (α := ℝ) 0 (-2) → GT.gt (α := ℝ) 2 0
⊢ LT.lt (α := ℝ) (-2) 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦
      HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-b * ‖x‖ ^ p))
h₁ :
  π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) =
    2 * π / p * b ^ (-HAdd.hAdd (α := ℝ) 0 2 / p) * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p)) =
    π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)

Tactic:
convert! (integral_rpow_mul_exp_neg_mul_rpow hp (by linarith : (-2 : ℝ) < 0)) hb using 1

Premises used: Complex.integral_rpow_mul_exp_neg_mul_rpow
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ 1 * rexp (-b * ‖x‖ ^ p))
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦
      HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-b * ‖x‖ ^ p))

Tactic:
simp_rw [rpow_zero, one_mul]

Premises used: Real.rpow_zero, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
linarith : p = 0 → -1 + (1 - p) + (p - 0) = 0
⊢ p ≠ 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
h : π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) =
    2 * π / p * b ^ (-HAdd.hAdd (α := ℝ) 0 2 / p) * Real.Gamma (HAdd.hAdd (α := ℝ) 0 2 / p)

Tactic:
rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]

Premises used: Real.Gamma_add_one, zero_add, div_ne_zero, two_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
simp_rw : Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)) L
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) A) : Filter ℝ≥0∞)

Tactic:
simp_rw [← MeasureTheory.lintegral_indicator_one A_mble,
           ← MeasureTheory.lintegral_indicator_one (As_mble _)]

Premises used: MeasureTheory.lintegral_indicator_one
-- Module: Mathlib.MeasureTheory.Integral.Indicator
Goal:
α : Type u_1
inst : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst_1 : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) B : ℝ≥0∞) (∞ : ℝ≥0∞)
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))

Tactic:
tendsto_lintegral_filter_of_dominated_convergence (B.indicator (1 : α → ℝ≥0∞))
          (Eventually.of_forall ?_) ?_ ?_ ?_

Premises used: Set.indicator, Filter.Eventually.of_forall, MeasureTheory.tendsto_lintegral_filter_of_dominated_convergence, OfNat.ofNat