awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
eq : ∀ (b : ℝ), a < b → Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
t2 :
  Tendsto.{0, u_1} (β := E) (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x • (g ∘ f) x) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x))
this : Ioi (f a) ⊆ f '' Ici a
t1 :
  Tendsto.{0, u_1} (β := E) ((fun (i : ℝ) ↦ ∫ (x : ℝ) in f a..id i, g x) ∘ f) atTop
    (𝓝 (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioi (f a))) fun (x : ℝ) ↦ g x))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x • (g ∘ f) x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (f a))) fun (u : ℝ) ↦ g u)

Tactic:
exact tendsto_nhds_unique (Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop a) eq) t2) t1

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, Filter.Tendsto.congr', tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (g ∘ f) x * f' x) (Ici a) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume

Tactic:
simpa [mul_comm] using hg2

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (g ∘ f) x * f' x) (Ici a) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume

Tactic:
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) := by simpa [mul_comm] using hg2
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (g ∘ f) x * f' x) (Ici a) volume
hg2' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ (g ∘ f) x * f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (f a))) fun (u : ℝ) ↦ g u)

Tactic:
simpa [mul_comm] using integral_deriv_smul_comp_Ioi hf hft hff' hg_cont hg1 hg2'

Premises used: mul_comm, MeasureTheory.integral_deriv_smul_comp_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
⊢ ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x

Tactic:
have a1 : ∀ x : ℝ, x ∈ S → HasDerivWithinAt (fun t : ℝ => t ^ p) (p * x ^ (p - 1)) S x :=
    fun x hx => (hasDerivAt_rpow_const (Or.inl (mem_Ioi.mp hx).ne')).hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
inl : ∀ (h : p < 0), InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
inr : ∀ (h : 0 < p), InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
rcases lt_or_gt_of_ne hp with (h | h)

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
inl : StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
apply StrictAntiOn.injOn

Premises used: StrictAntiOn.injOn
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
inl : x ^ (-p) < y ^ (-p)
⊢ LT.lt (α := ℝ) ((fun (x : ℝ) ↦ x ^ p) y) ((fun (x : ℝ) ↦ x ^ p) x)

Tactic:
rw [← inv_lt_inv₀ (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx),
        ← rpow_neg (le_of_lt hy)]

Premises used: Real.rpow_pos_of_pos, le_of_lt, Real.rpow_neg, inv_lt_inv₀
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)

Tactic:
rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)

Premises used: Iff.mpr, neg_pos, le_of_lt, Real.rpow_lt_rpow
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)

Tactic:
exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)

Premises used: Iff.mpr, neg_pos, le_of_lt, Real.rpow_lt_rpow
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : 0 < p
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
StrictMonoOn.injOn fun x hx y _ hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h

Premises used: StrictMonoOn.injOn, Set.mem_Ioi, LT.lt.le, Real.rpow_lt_rpow, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : 0 < p
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
exact StrictMonoOn.injOn fun x hx y _ hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h

Premises used: StrictMonoOn.injOn, Set.mem_Ioi, LT.lt.le, Real.rpow_lt_rpow, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
have a2 : InjOn (fun x : ℝ => x ^ p) S := by
    rcases lt_or_gt_of_ne hp with (h | h)
    · apply StrictAntiOn.injOn
      intro x hx y hy hxy
      rw [← inv_lt_inv₀ (rpow_pos_of_pos hx p) (rpow_pos_of_pos hy p), ← rpow_neg (le_of_lt hx),
        ← rpow_neg (le_of_lt hy)]
      exact rpow_lt_rpow (le_of_lt hx) hxy (neg_pos.mpr h)
    exact StrictMonoOn.injOn fun x hx y _ hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
h : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (t : ℝ) ↦ t ^ p) '' S) x ↔ x ∈ S
⊢ (fun (t : ℝ) ↦ t ^ p) '' S = S

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
h : (∃ x_1 ∈ S, x_1 ^ p = x) → x ∈ S
h₁ : x ∈ S → ∃ x_1 ∈ S, x_1 ^ p = x
⊢ (∃ x_1 ∈ S, x_1 ^ p = x) ↔ x ∈ S

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S

Tactic:
rpow_pos_of_pos hy p

Premises used: Real.rpow_pos_of_pos, Set.Ioi, Set.Mem, setOf
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S

Tactic:
exact rpow_pos_of_pos hy p

Premises used: Real.rpow_pos_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1 ∈ S, x_1 ^ p = x

Tactic:
⟨x ^ (1 / p), rpow_pos_of_pos hx _, ?_⟩

Premises used: Real.rpow_pos_of_pos, HDiv.hDiv, HPow.hPow, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
h : (x ^ (1 / p)) ^ p = x
⊢ ∃ x_1 ∈ S, x_1 ^ p = x

Tactic:
refine ⟨x ^ (1 / p), rpow_pos_of_pos hx _, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
h : x ^ (1 / p * p) = x
h₁ : HPow.hPow (β := ℝ) x 1 = x
h₂ h₃ : x = x
⊢ (x ^ (1 / p)) ^ p = x

Tactic:
rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]

Premises used: le_of_lt, Real.rpow_one, one_div_mul_cancel, Real.rpow_mul
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ (fun (t : ℝ) ↦ t ^ p) '' S = S

Tactic:
have a3 : (fun t : ℝ => t ^ p) '' S = S := by
    ext1 x; rw [mem_image]; constructor
    · rintro ⟨y, hy, rfl⟩; exact rpow_pos_of_pos hy p
    · intro hx; refine ⟨x ^ (1 / p), rpow_pos_of_pos hx _, ?_⟩
      rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (t : ℝ) ↦ t ^ p) '' Ioi 0))
      fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))

Tactic:
have := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi a1 a2 g
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (t : ℝ) ↦ t ^ p) '' Ioi 0))
      fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume S) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))

Tactic:
rw [a3] at this
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume S) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦ g y)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume S) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))

Tactic:
setIntegral_congr_fun measurableSet_Ioi ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume S) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))
refine :
  EqOn.{0, u_1} (β := E) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • g (x ^ p)) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • g (x ^ p))
    (Ioi 0)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume S) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      |p * x ^ (p - 1)| • g (x ^ p))
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : (|p| * x ^ (p - 1)) • g (x ^ p) = (|p| * |x ^ (p - 1)|) • g (x ^ p)
rw₁ rw₂ : (|p| * x ^ (p - 1)) • g (x ^ p) = (|p| * x ^ (p - 1)) • g (x ^ p)
⊢ (|p| * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)

Tactic:
rw [abs_mul, abs_of_nonneg (rpow_nonneg (le_of_lt hx) _)]

Premises used: abs_mul, le_of_lt, abs_of_nonneg, Real.rpow_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦ g y)

Tactic:
integral_comp_rpow_Ioi g hp.ne'

Premises used: MeasureTheory.integral_comp_rpow_Ioi, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
h : ∀ (x : ℝ), p = |p|
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (p * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦ g y)

Tactic:
convert! integral_comp_rpow_Ioi g hp.ne'

Premises used: MeasureTheory.integral_comp_rpow_Ioi, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
x : ℝ
h h₁ : p = p
⊢ p = |p|

Tactic:
rw [abs_of_nonneg hp.le]

Premises used: LT.lt.le, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ ∀ (c : ℝ), MeasurableSet (Ioi c)

Tactic:
have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ measurableSpace volume fun (x : ℝ) ↦ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ (Ioi (b * a)).indicator g (b * x))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ g (b * x)) =
    HSMul.hSMul (β := E) b⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (b * a))) fun (x : ℝ) ↦ g x)

Tactic:
rw [← integral_indicator (this a), ← integral_indicator (this (b * a)),
    ← abs_of_pos (inv_pos.mpr hb), ← Measure.integral_comp_mul_left]

Premises used: Iff.mpr, MeasureTheory.integral_indicator, HMul.hMul, inv_pos, MeasureTheory.Measure.integral_comp_mul_left, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
e_f :
  Eq.{u_1 + 1} (α := ℝ → E) (fun (x : ℝ) ↦ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x) fun (x : ℝ) ↦
    (Ioi (b * a)).indicator g (b * x)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ measurableSpace volume fun (x : ℝ) ↦ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ (Ioi (b * a)).indicator g (b * x))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
e_f : ∀ (x : ℝ), (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
⊢ Eq.{u_1 + 1} (α := ℝ → E) (fun (x : ℝ) ↦ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x) fun (x : ℝ) ↦
    (Ioi (b * a)).indicator g (b * x)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
e_f : (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = indicator (HMul.hMul b ⁻¹' Ioi (b * a)) (g ∘ HMul.hMul b) x
e_f₁ : (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a / b)).indicator (g ∘ HMul.hMul b) x
e_f₂ : (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi a).indicator (g ∘ HMul.hMul b) x
e_f₃ e_f₄ :
  Eq.{u_1 + 1} (α := E) ((Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x) ((Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x)
⊢ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)

Tactic:
rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ hb, mul_div_cancel_left₀ _ hb.ne',
    Function.comp_def]

Premises used: Set.preimage_const_mul_Ioi₀, mul_div_cancel_left₀, Set.indicator_comp_right, LT.lt.ne', Function.comp_def
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ g (x * b)) =
    HSMul.hSMul (β := E) b⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (a * b))) fun (x : ℝ) ↦ g x)

Tactic:
simpa only [mul_comm] using integral_comp_mul_left_Ioi g a hb

Premises used: mul_comm, MeasureTheory.integral_comp_mul_left_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
inl : ∀ (h : p < 0), InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
inr : ∀ (h : 0 < p), InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
rcases lt_or_gt_of_ne hp with (h | h)

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
inl : StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
apply StrictAntiOn.injOn

Premises used: StrictAntiOn.injOn