awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
have h : ∀ (x : ℝ), p = |p|
Tactic: convert! integral_comp_rpow_Ioi g hp.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
x : ℝ
⊢ p = |p|
have h : p = p
Tactic: rw [abs_of_nonneg hp.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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 (b * x)) =
    HSMul.hSMul (β := E) b⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (b * a))) fun (x : ℝ) ↦ g x)
have this : ∀ (c : ℝ), MeasurableSet (Ioi c)
Tactic: have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (@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)
have 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))
Tactic: rw [← integral_indicator (this a), ← integral_indicator (this (b * a)),
    ← abs_of_pos (inv_pos.mpr hb), ← Measure.integral_comp_mul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ 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)
have e_f : ∀ (x : ℝ), (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ
⊢ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
have e_f : (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = indicator (HMul.hMul b ⁻¹' Ioi (b * a)) (g ∘ HMul.hMul b) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ hb, mul_div_cancel_left₀ _ hb.ne',
    Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
have e_f₁ : (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a / b)).indicator (g ∘ HMul.hMul b) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ hb, mul_div_cancel_left₀ _ hb.ne',
    Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
have e_f₂ : (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi a).indicator (g ∘ HMul.hMul b) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ hb, mul_div_cancel_left₀ _ hb.ne',
    Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (Ioi a).indicator (fun (x : ℝ) ↦ g (b * x)) x = (Ioi (b * a)).indicator g (b * x)
have 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)
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ hb, mul_div_cancel_left₀ _ hb.ne',
    Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
have inl : ∀ (h : p < 0), InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
Tactic: rcases lt_or_gt_of_ne hp with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
have inr : ∀ (h : 0 < p), InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
Tactic: rcases lt_or_gt_of_ne hp with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
have inl : StrictAntiOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
Tactic: apply StrictAntiOn.injOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ LT.lt (α := ℝ) ((fun (x : ℝ) ↦ x ^ p) y) ((fun (x : ℝ) ↦ x ^ p) x)
have inl : x ^ (-p) < y ^ (-p)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
      (Ioi 0) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi 0) volume
have a2 : 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 _hy hxy => rpow_lt_rpow (mem_Ioi.mp hx).le hxy h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ (fun (t : ℝ) ↦ t ^ p) '' S = S
have h : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) ((fun (t : ℝ) ↦ t ^ p) '' S) x ↔ x ∈ S
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
⊢ (∃ x_1 ∈ S, x_1 ^ p = x) ↔ x ∈ S
have h : (∃ x_1 ∈ S, x_1 ^ p = x) → x ∈ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
h : (∃ x_1 ∈ S, x_1 ^ p = x) → x ∈ S
⊢ (∃ x_1 ∈ S, x_1 ^ p = x) ↔ x ∈ S
have h₁ : x ∈ S → ∃ x_1 ∈ S, x_1 ^ p = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
⊢ ∃ x_1 ∈ S, x_1 ^ p = x
have h : (x ^ (1 / p)) ^ p = x
Tactic: refine ⟨x ^ (1 / p), rpow_pos_of_pos hx _, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
⊢ (x ^ (1 / p)) ^ p = x
have h : x ^ (1 / p * p) = x
Tactic: rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
h : x ^ (1 / p * p) = x
⊢ (x ^ (1 / p)) ^ p = x
have h₁ : HPow.hPow (β := ℝ) x 1 = x
Tactic: rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
x : ℝ
hx : x ∈ S
h : x ^ (1 / p * p) = x
h₁ : HPow.hPow (β := ℝ) x 1 = x
⊢ (x ^ (1 / p)) ^ p = x
have h₂ : x = x
Tactic: rw [← rpow_mul (le_of_lt hx), one_div_mul_cancel hp, rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
      (Ioi 0) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi 0) volume
have a3 : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
      (Ioi 0) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi 0) volume
have this : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f ((fun (t : ℝ) ↦ t ^ p) '' Ioi 0) volume ↔
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
    (Ioi 0) volume
Tactic: have := integrableOn_image_iff_integrableOn_abs_deriv_smul measurableSet_Ioi a1 a2 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f ((fun (t : ℝ) ↦ t ^ p) '' Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
      (Ioi 0) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
      (Ioi 0) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi 0) volume
have this₁ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f S volume ↔
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
    (Ioi 0) volume
Tactic: rw [a3] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f S volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
      (Ioi 0) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
      (Ioi 0) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi 0) volume
have rw : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
    (Ioi 0) volume ↔
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
    (Ioi 0) volume
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f S volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
      (Ioi 0) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (|p| * x ^ (p - 1)) • f (x ^ p))
      (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
      (Ioi 0) volume
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), (|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)
Tactic: refine integrableOn_congr_fun (fun x hx => ?_) measurableSet_Ioi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
a2 : InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S
a3 : (fun (t : ℝ) ↦ t ^ p) '' S = S
this :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f S volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |p * x ^ (p - 1)| • f (x ^ p))
      (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)
have simp_rw : (|p| * x ^ (p - 1)) • f (x ^ p) = (|p| * |x ^ (p - 1)|) • f (x ^ p)
Tactic: simp_rw [abs_mul, abs_of_nonneg (rpow_nonneg (le_of_lt hx) _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f (a * x)) (Ioi c) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi (a * c)) volume
have rw : @Integrable.{u_1, 0} E _ _ _ measurableSpace ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) volume ↔
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi (a * c)) volume
Tactic: rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi c)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ @Integrable.{u_1, 0} E _ _ _ measurableSpace ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi (a * c)) volume
have rw : @Integrable.{u_1, 0} E _ _ _ measurableSpace ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) volume ↔
  @Integrable _ _ _ _ measurableSpace ((Ioi (a * c)).indicator f) volume
Tactic: rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi <| a * c)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ @Integrable.{u_1, 0} E _ _ _ measurableSpace ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) volume ↔
    @Integrable _ _ _ _ measurableSpace ((Ioi (a * c)).indicator f) volume
have h : Eq.{u_1 + 1} (α := ℝ → E) ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) fun (x : ℝ) ↦ (Ioi (a * c)).indicator f (a * x)
Tactic: convert! integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne' using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Eq.{u_1 + 1} (α := ℝ → E) ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) fun (x : ℝ) ↦ (Ioi (a * c)).indicator f (a * x)
have h : ∀ (x : ℝ), (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
have h : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = indicator (HMul.hMul a ⁻¹' Ioi (a * c)) (f ∘ HMul.hMul a) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ ha, mul_comm a c,
    mul_div_cancel_right₀ _ ha.ne', Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
h : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = indicator (HMul.hMul a ⁻¹' Ioi (a * c)) (f ∘ HMul.hMul a) x
⊢ (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
have h₁ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c / a)).indicator (f ∘ HMul.hMul a) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ ha, mul_comm a c,
    mul_div_cancel_right₀ _ ha.ne', Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
h : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = indicator (HMul.hMul a ⁻¹' Ioi (a * c)) (f ∘ HMul.hMul a) x
h₁ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c / a)).indicator (f ∘ HMul.hMul a) x
⊢ (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
have h₂ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (c * a / a)).indicator (f ∘ HMul.hMul a) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ ha, mul_comm a c,
    mul_div_cancel_right₀ _ ha.ne', Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
h : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = indicator (HMul.hMul a ⁻¹' Ioi (a * c)) (f ∘ HMul.hMul a) x
h₁ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c / a)).indicator (f ∘ HMul.hMul a) x
h₂ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (c * a / a)).indicator (f ∘ HMul.hMul a) x
⊢ (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
have h₃ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi c).indicator (f ∘ HMul.hMul a) x
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ ha, mul_comm a c,
    mul_div_cancel_right₀ _ ha.ne', Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
h : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = indicator (HMul.hMul a ⁻¹' Ioi (a * c)) (f ∘ HMul.hMul a) x
h₁ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c / a)).indicator (f ∘ HMul.hMul a) x
h₂ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (c * a / a)).indicator (f ∘ HMul.hMul a) x
h₃ : (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi c).indicator (f ∘ HMul.hMul a) x
⊢ (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
have h₄ : Eq.{u_1 + 1} (α := E) ((Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x) ((Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x)
Tactic: rw [← indicator_comp_right, preimage_const_mul_Ioi₀ _ ha, mul_comm a c,
    mul_div_cancel_right₀ _ ha.ne', Function.comp_def]