-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
/-- An even 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_even` for a stronger result. -/
lemma intervalIntegrable_of_even₀ (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:
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 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:
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:
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

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:
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)