awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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 : ℤ
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 : ℝ))))
⊢ ‖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 : ℝ))))

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]

Premises used: le_add_iff_nonneg_right, ContinuousMap.norm_le, add_sub_cancel_left, TopologicalSpace.Compacts.coe_mk, zero_le_one, Real.volume_real_Icc_of_le, mul_one, norm_nonneg, ContinuousMap.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
      ((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 : ℝ)) ⋯) :
        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⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
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 : ℝ)) ⋯) :
        E) ≤
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
⊢ 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:
simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk,
      sub_add_cancel] using this

Premises used: Subtype.coe_mk, ContinuousMap.coe_addRight, ContinuousMap.comp_apply, sub_add_cancel, ContinuousMap.restrict_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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 : ℝ))))
⊢ Eq (α := Set ℝ) (⋃ (i : ℤ), (↑{ carrier := Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), isCompact' := ⋯ } : Set ℝ))
    univ

Tactic:
iUnion_Icc_intCast ℝ

Premises used: Real, setOf, iUnion_Icc_intCast, Set.Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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 : ℝ))))
⊢ Eq (α := Set ℝ) (⋃ (i : ℤ), (↑{ carrier := Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), isCompact' := ⋯ } : Set ℝ))
    univ

Tactic:
exact iUnion_Icc_intCast ℝ

Premises used: Real, iUnion_Icc_intCast
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x

Tactic:
have A : MeasurableEmbedding fun x : ℝ => -x :=
    (Homeomorph.neg ℝ).isClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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 _ _ _ _ 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))
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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 _ _ _ _ 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

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.map_neg_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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))
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))
⊢ 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)

Tactic:
simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, neg_Ici, neg_neg]

Premises used: MeasureTheory.integral_Ici_eq_integral_Ioi, neg_neg, Set.neg_Ici, Set.neg_preimage
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
c : ℝ
f : ℝ → E
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)
⊢ 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)

Tactic:
rw [← neg_neg c, ← integral_comp_neg_Iic]

Premises used: neg_neg, integral_comp_neg_Iic
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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 (Iic (- - -c))) fun (x : ℝ) ↦ f x)

Tactic:
simp only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)

Tactic:
setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), f |x| = f x
⊢ 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:
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
hx

Premises used: Set.Ioi, Set.Mem
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
exact hx
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw rw₁ : f x = f x
⊢ f |x| = f x

Tactic:
rw [abs_eq_self.mpr (le_of_lt (by exact hx))]

Premises used: Iff.mpr, le_of_lt, abs_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)

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))]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
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)
⊢ (@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)

Premises used: Set.Ioi, abs, MeasureTheory.IntegrableOn, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
rw :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0)
    (Measure.map Neg.neg volume)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume

Tactic:
rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.map_neg_eq_self
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x := ⋯
rw :
  IntegrableOn (α := ℝ) (ε := ℝ) (mα := Real.measurableSpace) ((fun (x : ℝ) ↦ f |x|) ∘ fun (x : ℝ) ↦ -x)
    (preimage (β := ℝ) (fun (x : ℝ) ↦ -x) (Iic 0)) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0)
    (Measure.map Neg.neg volume)

Tactic:
rw [m.integrableOn_map_iff]

Premises used: MeasurableEmbedding.integrableOn_map_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x := ⋯
simp_rw : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f |x|) (Ici 0) volume
⊢ IntegrableOn (α := ℝ) (ε := ℝ) (mα := Real.measurableSpace) ((fun (x : ℝ) ↦ f |x|) ∘ fun (x : ℝ) ↦ -x)
    (preimage (β := ℝ) (fun (x : ℝ) ↦ -x) (Iic 0)) volume

Tactic:
simp_rw [Function.comp_def, abs_neg, neg_preimage, neg_Iic, neg_zero]

Premises used: abs_neg, Function.comp_def, Set.neg_preimage, neg_zero, Set.neg_Iic
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x := ⋯
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f |x|) (Ici 0) volume

Tactic:
Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi hf

Premises used: Iff.mpr, integrableOn_Ici_iff_integrableOn_Ioi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x := ⋯
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f |x|) (Ici 0) volume

Tactic:
exact Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi hf

Premises used: Iff.mpr, integrableOn_Ici_iff_integrableOn_Ioi
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume

Tactic:
have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) := by
      rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
      let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding
      rw [m.integrableOn_map_iff]
      simp_rw [Function.comp_def, abs_neg, neg_preimage, neg_Iic, neg_zero]
      exact Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi hf
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
rw :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0 ∪ Ioi 0)) fun (x : ℝ) ↦ f |x|)
rw₁ :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ) ↦ f |x|)
rw₂ rw₃ :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)

Tactic:
rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]

Premises used: MeasureTheory.setIntegral_union, le_rfl, Set.Iic_disjoint_Ioi, measurableSet_Ioi, Set.Iic_union_Ioi, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
rw :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x) =
    HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
⊢ HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)

Tactic:
rw [two_mul, eq]

Premises used: two_mul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
⊢ HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x) =
    HAdd.hAdd (α := ℝ)
      (@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:
congr! 1
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
h :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f (-x))
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)

Tactic:
rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]

Premises used: integral_comp_neg_Iic, neg_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f |x|)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0)) fun (x : ℝ) ↦ f (-x))

Tactic:
setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)

Premises used: measurableSet_Iic, MeasureTheory.setIntegral_congr_fun