-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
/-- An odd function is interval integrable (with respect to the volume measure) on every interval
of the form `0..x` if it is interval integrable (with respect to the volume measure) on every
interval of the form `0..x`, for positive `x`.

See `intervalIntegrable_of_odd` for a stronger result. -/
lemma intervalIntegrable_of_odd₀
    (h₁f : ∀ x, -f x = f (-x)) (h₂f : ∀ x, 0 < x → IntervalIntegrable f volume 0 x) (t : ℝ) :
    IntervalIntegrable f volume 0 t

Proof state:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable f volume 0 t

Tactic:
rw [IntervalIntegrable.iff_comp_neg]

Result:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable (fun x => f (-x)) volume (-0) (-t)

Proof state:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable (fun t => -f t) volume (-0) (-t)

Tactic:
apply IntervalIntegrable.neg

Result:
case inl.h
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable f volume (-0) (-t)

Proof state:
case inr.inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
exact h₂f t h

Result:
no goals

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
⊢ IntervalIntegrable f volume 0 t

Tactic:
rcases lt_trichotomy t 0 with h | h | h

Result:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable f volume 0 t

case inr.inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t = 0
⊢ IntervalIntegrable f volume 0 t

case inr.inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ 0 < -t

Tactic:
norm_num [h]

Result:
no goals

Proof state:
case inl.h
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable f volume (-0) (-t)

Tactic:
simp [h₂f (-t) (by norm_num [h])]

Result:
no goals

Proof state:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable (fun x => f (-x)) volume (-0) (-t)

Tactic:
conv => arg 1; intro t; rw [← h₁f]

Result:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t < 0
⊢ IntervalIntegrable (fun t => -f t) volume (-0) (-t)

Proof state:
case inr.inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
h : t = 0
⊢ IntervalIntegrable f volume 0 t

Tactic:
rw [h]

Result:
no goals