awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) (Ici a) volume
b : ℝ
hb : a < b
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
have i1 : Ioo (min a b) (max a b) ⊆ Ioi a
Tactic: have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ [[a, b]] ⊆ Ici a
have rw : Icc a b ⊆ Ici a
Tactic: rw [uIcc_of_le hb.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ Eq.{u_1 + 1} (α := E) (∫ (x : ℝ) in a..b, f' x • (g ∘ f) x) (∫ (u : ℝ) in f a..f b, g u)
have i2 : [[a, b]] ⊆ Ici a
Tactic: have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) (Ici a) volume
⊢ 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)
have 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)
Tactic: have eq : ∀ b : ℝ, a < b → (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u := fun b hb ↦ by
    have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
    have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
    refine
      intervalIntegral.integral_deriv_smul_comp''' (hf.mono i2)
        (fun x hx => hff' x <| mem_of_mem_of_subset hx i1) (hg_cont.mono <| image_mono ?_)
        (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2) <;> assumption
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) (Ici 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)
⊢ 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)
have hg2₁ : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ioi a) volume
Tactic: rw [integrableOn_Ici_iff_integrableOn_Ioi] at hg2
Cleared hypotheses: hg2, eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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)
⊢ 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)
have 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))
Tactic: have t2 := intervalIntegral_tendsto_integral_Ioi _ hg2 tendsto_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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))
⊢ 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)
have this : Ioi (f a) ⊆ f '' Ici a
Tactic: have : Ioi (f a) ⊆ f '' Ici a :=
    Ioi_subset_Ici_self.trans <|
      IsPreconnected.intermediate_value_Ici isPreconnected_Ici self_mem_Ici
        (le_principal_iff.mpr <| Ici_mem_atTop _) hf hft
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
⊢ 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)
have 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))
Tactic: have t1 := (intervalIntegral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
⊢ 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)
have hg2' : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := 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 (y : ℝ) ↦ g y)
have a1 : ∀ 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
-- 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 : 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
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
⊢ 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
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
⊢ 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
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
⊢ 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
g : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun (t : ℝ) ↦ t ^ p) (p * x ^ (p - 1)) S x
⊢ 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 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 _ 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
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
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
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 : ℝ
⊢ (∃ 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
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
⊢ (∃ 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
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
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
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 / 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
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 / 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
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
⊢ (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
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
⊢ 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 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
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 (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦ g y)
have 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))
Tactic: have := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi a1 a2 g
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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 (Ioi 0)) fun (x : ℝ) ↦
      (|p| * x ^ (p - 1)) • g (x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (y : ℝ) ↦ g y)
have 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))
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
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 (y : ℝ) ↦ g y)
have 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))
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
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))
have 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)
Tactic: refine setIntegral_congr_fun 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
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
⊢ (|p| * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)
have rw : (|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) _)]
-- 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 : 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)
⊢ (|p| * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)
have rw₁ : (|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) _)]