awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) volume
have rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0) (Measure.map Neg.neg volume)
Tactic: rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
-- 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)
hf : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
m : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ -x := ⋯
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Iic 0)
    (Measure.map Neg.neg volume)
have rw : IntegrableOn (α := ℝ) (ε := ℝ) (mα := Real.measurableSpace) ((fun (x : ℝ) ↦ f |x|) ∘ fun (x : ℝ) ↦ -x)
  (preimage (β := ℝ) (fun (x : ℝ) ↦ -x) (Iic 0)) volume
Tactic: rw [m.integrableOn_map_iff]
-- 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)
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|) ∘ fun (x : ℝ) ↦ -x)
    (preimage (β := ℝ) (fun (x : ℝ) ↦ -x) (Iic 0)) volume
have simp_rw : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f |x|) (Ici 0) volume
Tactic: simp_rw [Function.comp_def, abs_neg, neg_preimage, neg_Iic, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have int_Iic : 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
-- 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)
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
⊢ (@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|)
have rw : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic 0 ∪ 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]
-- 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)
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|)
⊢ (@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|)
have rw₁ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ) ↦ f |x|)
Tactic: rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]
-- 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)
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|)
⊢ (@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|)
have rw₂ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|)
Tactic: rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]
-- 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)
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
⊢ 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)
have 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)
Tactic: rw [two_mul, eq]
-- 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)
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
⊢ 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)
have 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)
Tactic: congr! 1
-- 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)
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 (Ioi 0)) fun (x : ℝ) ↦ f x)
have 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))
Tactic: rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
-- 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)
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))
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic 0) x), f |x| = f (-x)
Tactic: refine setIntegral_congr_fun measurableSet_Iic (fun _ 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)
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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
⊢ f |x| = f (-x)
have h : f (-x) = f (-x)
Tactic: rw [abs_eq_neg_self.mpr (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)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have _ : (@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: calc
      _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
        rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]
      _ = 2 * ∫ x in Ioi 0, f x := by
        rw [two_mul, eq]
        congr! 1
        rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
        refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)
        rw [abs_eq_neg_self.mpr (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)
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
_ :
  (@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|)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have _₁ : 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: calc
      _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
        rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]
      _ = 2 * ∫ x in Ioi 0, f x := by
        rw [two_mul, eq]
        congr! 1
        rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
        refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)
        rw [abs_eq_neg_self.mpr (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)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
⊢ ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
have contrapose : ∀ (hf : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Integral (hypothesis)
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f x)
have this : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
Tactic: have : ¬ Integrable (fun x => f |x|) := by
      contrapose hf
      exact hf.integrableOn
-- 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)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
this : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
⊢ (@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 : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
  HMul.hMul (α := ℝ) 2
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
Tactic: rw [← eq, integral_undef hf, integral_undef this, mul_zero]
-- 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)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
this : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
neg :
  (@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₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) = HMul.hMul (α := ℝ) 2 0
Tactic: rw [← eq, integral_undef hf, integral_undef this, mul_zero]
-- 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)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
this : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
neg :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
neg₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) = HMul.hMul (α := ℝ) 2 0
⊢ (@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₂ : 0 = HMul.hMul (α := ℝ) 2 0
Tactic: rw [← eq, integral_undef hf, integral_undef this, mul_zero]
-- 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)
hf : ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f |x|) (Ioi 0) volume
this : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ f |x|) volume
neg :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) =
    HMul.hMul (α := ℝ) 2
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ f |x|)
neg₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f |x|) = HMul.hMul (α := ℝ) 2 0
neg₂ : 0 = HMul.hMul (α := ℝ) 2 0
⊢ (@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₃ : Eq (α := ℝ) 0 0
Tactic: rw [← eq, integral_undef hf, integral_undef this, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inl : ∀ (hE : Subsingleton E),
  (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
Tactic: obtain hE | hE := subsingleton_or_nontrivial E
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
p : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hp : 0 < p
inl :
  ∀ (hE : Subsingleton E),
    (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
      ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
⊢ (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
have inr : ∀ (hE : Nontrivial E),
  (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) =
    ENNReal.ofReal ((∫ (x : E), Real.exp (-‖x‖ ^ p) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p + 1))
Tactic: obtain hE | hE := subsingleton_or_nontrivial E