awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty
have h₁ : ∀ (a : ℝ),
  0 <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t')) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t') : ℝ≥0∞) →
    (s ∩ ({x} + a • t)).Nonempty
Tactic: filter_upwards [(tendsto_order.1
          (tendsto_addHaar_inter_smul_one_of_density_one μ s x h t' t'_meas t'pos.ne' t'top.ne)).1
      0 zero_lt_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
⊢ (s ∩ ({x} + r • t)).Nonempty
have this : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ (s ∩ ({x} + r • t')) ≠ 0 := fun h' => by
    simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (s ∩ ({x} + r • t)).Nonempty
have this₁ : (s ∩ ({x} + r • t')).Nonempty
Tactic: have : (s ∩ ({x} + r • t')).Nonempty := nonempty_of_measure_ne_zero this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
this_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
this : (s ∩ ({x} + r • t')).Nonempty
⊢ (s ∩ ({x} + r • t)).Nonempty
have apply : {x} + r • t' ⊆ {x} + r • t
Tactic: apply this.mono (inter_subset_inter Subset.rfl _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ENNReal) (regionBetween f g s) =
    ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
have h : g - f =ᶠ[ae (μ.restrict s)] fun (x : α) ↦ (↑(g x - f x).toNNReal : ℝ)
Tactic: have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
    hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun (x : α) ↦ (↑(g x - f x).toNNReal : ℝ)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ENNReal) (regionBetween f g s) =
    ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
have rw : (ae (μ.restrict s)).EventuallyEq (β := ENNReal) (fun (y : α) ↦ ENNReal.ofReal ((g - f) y)) fun (a : α) ↦
  (↑(g a - f a).toNNReal : ENNReal)
Tactic: rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs,
    integral_congr_ae h, lintegral_congr_ae,
    lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
hf :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
⊢ @Integrable E _ _ ℝ MeasureSpace.toMeasurableSpace (⇑f : (a : ℝ) → E) volume
have refine_1 : ∀ (n : ℤ),
  ‖ContinuousMap.restrict
          (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := sorry : Compacts ℝ } : Set ℝ) f‖ *
      Measure.real (m := MeasureSpace.toMeasurableSpace) volume
        (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := sorry : Compacts ℝ } : Set ℝ) ≤
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
Tactic: refine integrable_of_summable_norm_restrict (.of_nonneg_of_le
    (fun n : ℤ => mul_nonneg (norm_nonneg
      (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
        ENNReal.toReal_nonneg) (fun n => ?_) hf) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
hf :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
refine_1 :
  ∀ (n : ℤ),
    ‖ContinuousMap.restrict
            (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := ⋯ : Compacts ℝ } : Set ℝ) f‖ *
        Measure.real (m := MeasureSpace.toMeasurableSpace) volume
          (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := ⋯ : Compacts ℝ } : Set ℝ) ≤
      Norm.norm (E := C((↑(Icc 0 1) : Type), E))
        (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
⊢ @Integrable E _ _ ℝ MeasureSpace.toMeasurableSpace (⇑f : (a : ℝ) → E) volume
have refine_2 : Eq (α := Set ℝ) (⋃ (i : ℤ), (↑{ carrier := Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), isCompact' := sorry } : Set ℝ))
  univ
Tactic: refine integrable_of_summable_norm_restrict (.of_nonneg_of_le
    (fun n : ℤ => mul_nonneg (norm_nonneg
      (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
        ENNReal.toReal_nonneg) (fun n => ?_) hf) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
hf :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
n : ℤ
⊢ ‖ContinuousMap.restrict
          (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := ⋯ : Compacts ℝ } : Set ℝ) f‖ *
      Measure.real (m := MeasureSpace.toMeasurableSpace) volume
        (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := ⋯ : Compacts ℝ } : Set ℝ) ≤
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
have refine_1 : ∀ (x : (↑(Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) : Type)),
  Norm.norm (E := E) ((f : (a : ℝ) → E) (↑x : ℝ) : E) ≤
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
Tactic: simp only [Compacts.coe_mk, le_add_iff_nonneg_right, zero_le_one, volume_real_Icc_of_le,
      add_sub_cancel_left, mul_one, norm_le _ (norm_nonneg _), ContinuousMap.restrict_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
hf :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
n : ℤ
x : (↑(Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) : Type)
⊢ Norm.norm (E := E) ((f : (a : ℝ) → E) (↑x : ℝ) : E) ≤
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
have this : Norm.norm (E := E)
    ((ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))) : (a : (↑(Icc 0 1) : Type)) → E)
        (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) ((↑x : ℝ) - (↑n : ℝ)) sorry) :
      E) ≤
  Norm.norm (E := C((↑(Icc 0 1) : Type), E))
    (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
Tactic: have := ((f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)).norm_coe_le_norm
        ⟨x - n, ⟨sub_nonneg.mpr x.2.1, sub_le_iff_le_add'.mpr x.2.2⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
Tactic: have A : MeasurableEmbedding fun x : ℝ => -x :=
    (Homeomorph.neg ℝ).isClosedEmbedding.measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have this : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.map (fun (x : ℝ) ↦ -x) volume) (Ici (-c)))
    fun (y : ℝ) ↦ f y)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
    fun (x : ℝ) ↦ f (-x))
Tactic: have := MeasurableEmbedding.setIntegral_map (μ := volume) A f (Ici (-c))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
this :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.map (fun (x : ℝ) ↦ -x) volume) (Ici (-c)))
      fun (y : ℝ) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have this₁ : Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ici (-c))) fun (y : ℝ) ↦ f y)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
    fun (x : ℝ) ↦ f (-x))
Tactic: rw [Measure.map_neg_eq_self (volume : Measure ℝ)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ici (-c))) fun (y : ℝ) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have simp_rw : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (-c))) fun (x : ℝ) ↦ f x)
Tactic: simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ici (-c))) fun (y : ℝ) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
simp_rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (-c))) fun (x : ℝ) ↦ f x)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have simp_rw₁ : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
    fun (x : ℝ) ↦ f (-x))
Tactic: simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ici (-c))) fun (y : ℝ) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
simp_rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (-c))) fun (x : ℝ) ↦ f x)
simp_rw₁ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have simp_rw₂ : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (-Ici (-c))) fun (x : ℝ) ↦ f (-x))
Tactic: simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x
this :
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ici (-c))) fun (y : ℝ) ↦ f y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
simp_rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (-c))) fun (x : ℝ) ↦ f x)
simp_rw₁ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ((fun (x : ℝ) ↦ -x) ⁻¹' Ici (-c)))
      fun (x : ℝ) ↦ f (-x))
simp_rw₂ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (-Ici (-c))) fun (x : ℝ) ↦ f (-x))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (-c))) fun (x : ℝ) ↦ f x)
have simp_rw₃ : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ f (-x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic (- -c))) fun (x : ℝ) ↦ f (-x))
Tactic: simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦ f (-x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic (-c))) fun (x : ℝ) ↦ f x)
have rw : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic (-c))) fun (x : ℝ) ↦ f (- -x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic (- - -c))) fun (x : ℝ) ↦ f x)
Tactic: rw [← neg_neg c, ← integral_comp_neg_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
f : ℝ → ℝ
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), f |x| = f x
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ f |x| = f x
have rw : f x = f x
Tactic: rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
Goal:
f : ℝ → ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have eq : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
Tactic: have eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x := by
    refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
    rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have pos : ∀ (hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
Tactic: by_cases hf : IntegrableOn (fun x => f |x|) (Ioi 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (goal)
Goal:
f : ℝ → ℝ
eq :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
pos :
  ∀ (hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
      HMul.hMul (α := ℝ) 2
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have neg : ∀ (hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
Tactic: by_cases hf : IntegrableOn (fun x => f |x|) (Ioi 0)