-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_comp_rpow_iff [NormedSpace ℝ E] (f : ℝ → E) {p : ℝ} (hp : p ≠ 0) :
    IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Tactic:
have := integrableOn_image_iff_integrableOn_abs_deriv_smul measurableSet_Ioi a1 a2 f

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this :
  IntegrableOn f ((fun t => t ^ p) '' Ioi 0) volume ↔
    IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Proof state:
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ S → ∃ x_1 ∈ S, x_1 ^ p = x

Tactic:
intro hx

Result:
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1 ∈ S, x_1 ^ p = x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Tactic:
let S := Ioi (0 : ℝ)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Proof state:
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x

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

Result:
no goals

Proof state:
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
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)

Result:
no goals

Proof state:
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1 ∈ S, x_1 ^ p = x

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

Result:
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Tactic:
rw [this]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
a3 : (fun t => t ^ p) '' S = S
this : IntegrableOn f S volume ↔ IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume
⊢ IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Ioi 0) volume ↔
    IntegrableOn (fun x => |p * x ^ (p - 1)| • f (x ^ p)) (Ioi 0) volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ InjOn (fun x => x ^ p) S

Tactic:
rcases lt_or_gt_of_ne hp with (h | h)

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ InjOn (fun x => x ^ p) S

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ InjOn (fun x => x ^ p) S

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ x ∈ (fun t => t ^ p) '' S ↔ x ∈ S

Tactic:
rw [mem_image]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1 ∈ S, x_1 ^ p = x) ↔ x ∈ S

Proof state:
case h.mp.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S

Tactic:
exact rpow_pos_of_pos hy p

Result:
no goals

Proof state:
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ (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)]

Result:
case inl.H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ x ^ (-p) < y ^ (-p)

Proof state:
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
x : ℝ
⊢ (∃ x_1 ∈ S, x_1 ^ p = x) → x ∈ S

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case h.mp.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
a2 : InjOn (fun x => x ^ p) S
y : ℝ
hy : y ∈ S
⊢ y ^ p ∈ S