-- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
theorem integral_comp_abs {f : ℝ → ℝ} :
    ∫ x, f |x| = 2 * ∫ x in Ioi (0 : ℝ), f x

Proof state:
case h.e'_5
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ) in Iic 0, f |x| = ∫ (x : ℝ) in Iic 0, f (-x)

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

Result:
case h.e'_5
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
x✝ : ℝ
hx : x✝ ∈ Iic 0
⊢ f |x✝| = f (-x✝)

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f |x|

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

Result:
no goals

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ IntegrableOn (fun x => f |x|) (Iic 0) (Measure.map Neg.neg volume)

Tactic:
let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x => -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn (fun x => f |x|) (Iic 0) (Measure.map Neg.neg volume)

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f x = (∫ (x : ℝ) in Ioi 0, f x) + ∫ (x : ℝ) in Ioi 0, f x

Tactic:
congr! 1

Result:
case h.e'_5
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ) in Iic 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x

Proof state:
case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x => f |x|) (Ioi 0) volume
this : ¬Integrable (fun x => f |x|) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
rw [← eq, integral_undef hf, integral_undef this, mul_zero]

Result:
no goals

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
by_cases hf : IntegrableOn (fun x => f |x|) (Ioi 0)

Result:
case pos
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
rw [two_mul, eq]

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f x = (∫ (x : ℝ) in Ioi 0, f x) + ∫ (x : ℝ) in Ioi 0, f x

Proof state:
f : ℝ → ℝ
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < x✝

Tactic:
exact hx

Result:
no goals

Proof state:
f : ℝ → ℝ
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, 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))]

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Proof state:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x

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

Result:
f : ℝ → ℝ
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ f |x✝| = f x✝

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ IntegrableOn (fun x => f |x|) (Iic 0) volume

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

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ IntegrableOn (fun x => f |x|) (Iic 0) (Measure.map Neg.neg volume)

Proof state:
case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
have : ¬ Integrable (fun x => f |x|) := by
  contrapose! hf
  exact hf.integrableOn

Result:
case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x => f |x|) (Ioi 0) volume
this : ¬Integrable (fun x => f |x|) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Proof state:
case pos
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

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 integrableOn_Ici_iff_integrableOn_Ioi.mpr hf

Result:
case pos
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Proof state:
case h.e'_5
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ) in Iic 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x

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

Result:
case h.e'_5
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x => f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ) in Iic 0, f |x| = ∫ (x : ℝ) in Iic 0, f (-x)

Proof state:
f : ℝ → ℝ
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ f |x✝| = f x✝

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

Result:
no goals

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x => -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn ((fun x => f |x|) ∘ fun x => -x) ((fun x => -x) ⁻¹' Iic 0) volume

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

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x => f |x|) (Ioi 0) volume
m : MeasurableEmbedding fun x => -x := Homeomorph.measurableEmbedding (Homeomorph.neg ℝ)
⊢ IntegrableOn (fun x => f |x|) (Ici 0) volume

Proof state:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x => f |x|) (Ioi 0) volume
⊢ ¬Integrable (fun x => f |x|) volume

Tactic:
contrapose! hf

Result:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : Integrable (fun x => f |x|) volume
⊢ IntegrableOn (fun x => f |x|) (Ioi 0) volume