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 : ℝ → 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
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:
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
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)

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
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 : 0 < p
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
StrictMonoOn.injOn fun x hx y _hy 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
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 : 0 < p
⊢ InjOn (β := ℝ) (fun (x : ℝ) ↦ x ^ p) S

Tactic:
exact StrictMonoOn.injOn fun x hx y _hy 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
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:
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
-- 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
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
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
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
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:
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
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

Premises used: Real.rpow_pos_of_pos
-- 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
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
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 ∈ 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
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
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
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

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
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 (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
-- 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
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 (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
-- 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
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
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
⊢ 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

Tactic:
rw [this]
-- 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
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

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

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_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
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
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    (|p| * x ^ (p - 1)) • f (x ^ p) = |p * x ^ (p - 1)| • f (x ^ p)
⊢ 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:
refine integrableOn_congr_fun (fun x hx => ?_) measurableSet_Ioi

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_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
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
simp_rw : (|p| * x ^ (p - 1)) • f (x ^ p) = (|p| * |x ^ (p - 1)|) • f (x ^ p)
⊢ (|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) _)]

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
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (p - 1) • f (x ^ p)) (Ioi 0)
      volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi 0) volume

Tactic:
simpa only [← integrableOn_Ioi_comp_rpow_iff f hp, mul_smul] using
    (integrable_smul_iff (abs_pos.mpr hp).ne' _).symm

Premises used: Iff.mpr, LT.lt.ne', abs_pos, MeasureTheory.integrable_smul_iff, MeasureTheory.integrableOn_Ioi_comp_rpow_iff, Iff.symm, SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
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
⊢ 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

Tactic:
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi c)]

Premises used: measurableSet_Ioi, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
rw :
  @Integrable.{u_1, 0} E _ _ _ measurableSpace ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) volume ↔
    @Integrable _ _ _ _ measurableSpace ((Ioi (a * c)).indicator f) volume
⊢ @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 <| a * c)]

Premises used: measurableSet_Ioi, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (Ioi (a * c)).indicator f (a * x)) volume ↔
    @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace ((Ioi (a * c)).indicator f) volume

Tactic:
integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne'

Premises used: Set.Ioi, HMul.hMul, Set.indicator, MeasureTheory.integrable_comp_mul_left_iff, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
h :
  Eq.{u_1 + 1} (α := ℝ → E) ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) fun (x : ℝ) ↦ (Ioi (a * c)).indicator f (a * x)
⊢ @Integrable.{u_1, 0} E _ _ _ measurableSpace ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) volume ↔
    @Integrable _ _ _ _ measurableSpace ((Ioi (a * c)).indicator f) volume

Tactic:
convert! integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne' using 2

Premises used: Set.Ioi, HMul.hMul, Set.indicator, MeasureTheory.integrable_comp_mul_left_iff, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
h : ∀ (x : ℝ), (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (a * x)
⊢ Eq.{u_1 + 1} (α := ℝ → E) ((Ioi c).indicator fun (x : ℝ) ↦ f (a * x)) fun (x : ℝ) ↦ (Ioi (a * c)).indicator f (a * x)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h₄ h₅ :
  Eq.{u_1 + 1} (α := E) ((Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x) ((Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x)
⊢ (Ioi c).indicator (fun (x : ℝ) ↦ f (a * x)) x = (Ioi (a * c)).indicator f (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]

Premises used: Set.preimage_const_mul_Ioi₀, Set.indicator_comp_right, LT.lt.ne', mul_div_cancel_right₀, Function.comp_def, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 (x * a)) (Ioi c) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi (c * a)) volume

Tactic:
simpa only [mul_comm, mul_zero] using integrableOn_Ioi_comp_mul_left_iff f c ha

Premises used: MeasureTheory.integrableOn_Ioi_comp_mul_left_iff, MulZeroClass.mul_zero, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst_6 : CompleteSpace G
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦
      HAdd.hAdd (α := G) (β := G) ((((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x) : G)
        ((((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x) : G))
    volume
h_bot : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atTop (𝓝 n)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HAdd.hAdd (α := G) (β := G) ((((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x) : G)
        ((((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x) : G)) =
    n - m

Tactic:
integral_of_hasDerivAt_of_tendsto (fun x ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
    huv h_bot h_top

Premises used: MeasureTheory.integral_of_hasDerivAt_of_tendsto, ContinuousLinearMap.hasDerivAt_of_bilinear
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst_6 : CompleteSpace G
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
h_bot : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atTop (𝓝 n)
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
      HAdd.hAdd (α := G) (β := G) ((((L : (a : E) → F →L[ℝ] G) (u a) : F →L[ℝ] G) : (a : F) → G) (v' a) : G)
        ((((L : (a : E) → F →L[ℝ] G) (u' a) : F →L[ℝ] G) : (a : F) → G) (v a) : G)) =
    n - m
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) =
    n - m -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)

Tactic:
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]

Premises used: eq_sub_iff_add_eq, MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst_6 : CompleteSpace G
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
h_bot : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atTop (𝓝 n)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
      HAdd.hAdd (α := G) (β := G) ((((L : (a : E) → F →L[ℝ] G) (u a) : F →L[ℝ] G) : (a : F) → G) (v' a) : G)
        ((((L : (a : E) → F →L[ℝ] G) (u' a) : F →L[ℝ] G) : (a : F) → G) (v a) : G)) =
    n - m

Tactic:
integral_bilinear_hasDerivAt_eq_sub hu hv (huv'.add hu'v) h_bot h_top

Premises used: MeasureTheory.Integrable.add, MeasureTheory.integral_bilinear_hasDerivAt_eq_sub
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst_6 : CompleteSpace G
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
h_bot : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atTop (𝓝 n)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
      HAdd.hAdd (α := G) (β := G) ((((L : (a : E) → F →L[ℝ] G) (u a) : F →L[ℝ] G) : (a : F) → G) (v' a) : G)
        ((((L : (a : E) → F →L[ℝ] G) (u' a) : F →L[ℝ] G) : (a : F) → G) (v a) : G)) =
    n - m

Tactic:
exact integral_bilinear_hasDerivAt_eq_sub hu hv (huv'.add hu'v) h_bot h_top

Premises used: MeasureTheory.Integrable.add, MeasureTheory.integral_bilinear_hasDerivAt_eq_sub