awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c + x)) volume (a - c) (b - c)

Tactic:
simpa [add_comm] using IntervalIntegrable.comp_add_right hf c h

Premises used: IntervalIntegrable.comp_add_right, add_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
simp_rw :
  IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c + x)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b

Tactic:
simp_rw [add_comm c]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : IntervalIntegrable f volume (a - c + c) (b - c + c) ↔ IntervalIntegrable f volume a b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c) ↔ IntervalIntegrable f volume a b

Tactic:
rw [IntervalIntegrable.comp_add_right_iff (by grind)]

Premises used: IntervalIntegrable.comp_add_right_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume (a - c + c) (b - c + c) ↔ IntervalIntegrable f volume a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x - c)) volume (a + c) (b + c)

Tactic:
simpa only [sub_neg_eq_add] using IntervalIntegrable.comp_add_right hf (-c) h

Premises used: IntervalIntegrable.comp_add_right, Neg.neg, sub_neg_eq_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
simp_rw :
  IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + -c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x - c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min (a + c) (b + c) + -c)‖ₑ ≠ ∞

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : IntervalIntegrable f volume (a + c + -c) (b + c + -c) ↔ IntervalIntegrable f volume a b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + -c)) volume (a + c) (b + c) ↔ IntervalIntegrable f volume a b

Tactic:
rw [IntervalIntegrable.comp_add_right_iff (by grind)]

Premises used: IntervalIntegrable.comp_add_right_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume (a + c + -c) (b + c + -c) ↔ IntervalIntegrable f volume a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (-1 * min (a / -1) (b / -1))‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
rw :
  IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-a) (-b)
⊢ IntervalIntegrable f volume a b ↔ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-a) (-b)

Tactic:
rw [← comp_mul_left_iff (neg_ne_zero.2 one_ne_zero) h (by simp)]

Premises used: Iff.mpr, IntervalIntegrable.comp_mul_left_iff, neg_ne_zero, one_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-1 * x)) volume (a / -1) (b / -1) ↔
    IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-a) (-b)

Tactic:
simp [div_neg]

Premises used: div_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (c + min (a - c) (b - c))‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (c - x)) volume (c - a) (c - b)

Tactic:
simpa only [neg_sub, ← sub_eq_add_neg] using (iff_comp_neg (by simp)).mp (hf.comp_add_left c h)

Premises used: neg_sub, sub_eq_add_neg, IntervalIntegrable.comp_add_left, Iff.mp, IntervalIntegrable.iff_comp_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
c : ℝ
h_1 : ‖f (min a b)‖ₑ ≠ ∞
h : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (c - x)) volume (c - a) (c - b)
⊢ IntervalIntegrable f volume a b

Tactic:
simpa using h.comp_sub_left c

Premises used: IntervalIntegrable.comp_sub_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
u : ℝ → E
a b : ℝ
hu : ContinuousOn u [[a, b]]
⊢ IntervalIntegrable u μ a b

Tactic:
(ContinuousOn.integrableOn_Icc hu).intervalIntegrable

Premises used: ContinuousOn.integrableOn_Icc, MeasureTheory.IntegrableOn.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
u : ℝ → E
a b : ℝ
h : a ≤ b
hu : ContinuousOn u (Icc a b)
⊢ IntervalIntegrable u μ a b

Tactic:
ContinuousOn.intervalIntegrable ((uIcc_of_le h).symm ▸ hu)

Premises used: Set.uIcc_of_le, Eq.rec, ContinuousOn.intervalIntegrable, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
u : ℝ → E
hu : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
a b : ℝ
⊢ IntervalIntegrable u μ a b

Tactic:
hu.continuousOn.intervalIntegrable

Premises used: Continuous.continuousOn, ContinuousOn.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
rw : IntegrableOn u (Ι a b) μ
⊢ IntervalIntegrable u μ a b

Tactic:
rw [intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b) μ

Tactic:
(hu.integrableOn_isCompact isCompact_uIcc).mono_set Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono_set, MonotoneOn.integrableOn_isCompact
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b) μ

Tactic:
exact (hu.integrableOn_isCompact isCompact_uIcc).mono_set Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono_set, MonotoneOn.integrableOn_isCompact
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : AntitoneOn u [[a, b]]
⊢ IntervalIntegrable u μ a b

Tactic:
hu.dual_right.intervalIntegrable

Premises used: MonotoneOn.intervalIntegrable, AntitoneOn.dual_right, OrderDual
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : Monotone u
⊢ IntervalIntegrable u μ a b

Tactic:
(hu.monotoneOn _).intervalIntegrable

Premises used: MonotoneOn.intervalIntegrable, Monotone.monotoneOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
inst_2 : ConditionallyCompleteLinearOrder E
inst_3 : OrderTopology E
inst_4 : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : Antitone u
⊢ IntervalIntegrable u μ a b

Tactic:
(hu.antitoneOn _).intervalIntegrable

Premises used: Antitone.antitoneOn, AntitoneOn.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
inr : ∀ (h : t = 0), IntervalIntegrable f volume 0 t
inr₁ : ∀ (h : 0 < t), IntervalIntegrable f volume 0 t
⊢ IntervalIntegrable f volume 0 t

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

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
inl : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
⊢ IntervalIntegrable f volume 0 t

Tactic:
rw [IntervalIntegrable.iff_comp_neg ht]

Premises used: IntervalIntegrable.iff_comp_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
arg : fun (x : ℝ) ↦ f (-x)
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)

Tactic:
arg 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t_1 : ℝ
ht : ‖f (min 0 t_1)‖ₑ ≠ ∞
h : t_1 < 0
t : ℝ
h₁ : f t
| f (-t)

Tactic:
rw [← h₁f]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
h₁ : ∀ (t : ℝ), f t
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)

Tactic:
arg 1; intro t; rw [← h₁f]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
inl : IntervalIntegrable f volume (-0) (-t)
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)

Tactic:
conv => arg 1; intro t; rw [← h₁f]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ 0 < -t

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable f volume (-0) (-t)

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

Premises used: Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t = 0
inr inr₁ : IntervalIntegrable f volume 0 0
⊢ IntervalIntegrable f volume 0 t

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
h₂f t h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
exact h₂f t h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
a b : ℝ
ha : ‖f (min 0 a)‖ₑ ≠ ∞
hb : ‖f (min 0 b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume a b

Tactic:
(intervalIntegrable_of_even₀ h₁f h₂f ha).symm.trans (b := 0)
    (intervalIntegrable_of_even₀ h₁f h₂f hb)

Premises used: intervalIntegrable_of_even₀, IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
inl : ∀ (h : t < 0), IntervalIntegrable f volume 0 t
inr : ∀ (h : t = 0), IntervalIntegrable f volume 0 t
inr₁ : ∀ (h : 0 < t), IntervalIntegrable f volume 0 t
⊢ IntervalIntegrable f volume 0 t

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

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
inl : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)
⊢ IntervalIntegrable f volume 0 t

Tactic:
rw [IntervalIntegrable.iff_comp_neg]

Premises used: IntervalIntegrable.iff_comp_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
arg : fun (x : ℝ) ↦ f (-x)
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)

Tactic:
arg 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t_1 : ℝ
ht : ‖f (min 0 t_1)‖ₑ ≠ ∞
h : t_1 < 0
t : ℝ
h₁ : -f t
| f (-t)

Tactic:
rw [← h₁f]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
h₁ : ∀ (t : ℝ), -f t
| IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)

Tactic:
arg 1; intro t; rw [← h₁f]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
inl : IntervalIntegrable.{u_5} (ε := E) (fun (t : ℝ) ↦ -f t) volume (-0) (-t)
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (-x)) volume (-0) (-t)

Tactic:
conv => arg 1; intro t; rw [← h₁f]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
inl : IntervalIntegrable f volume (-0) (-t)
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (t : ℝ) ↦ -f t) volume (-0) (-t)

Tactic:
apply IntervalIntegrable.neg

Premises used: IntervalIntegrable.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ 0 < -t

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t < 0
⊢ IntervalIntegrable f volume (-0) (-t)

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

Premises used: Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : t = 0
inr inr₁ : IntervalIntegrable f volume 0 0
⊢ IntervalIntegrable f volume 0 t

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
h₂f t h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
t : ℝ
ht : ‖f (min 0 t)‖ₑ ≠ ∞
h : 0 < t
⊢ IntervalIntegrable f volume 0 t

Tactic:
exact h₂f t h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
h₁f : ∀ (x : ℝ), -f x = f (-x)
h₂f : ∀ (x : ℝ), 0 < x → IntervalIntegrable f volume 0 x
a b : ℝ
ha : ‖f (min 0 a)‖ₑ ≠ ∞
hb : ‖f (min 0 b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f volume a b

Tactic:
(intervalIntegrable_of_odd₀ h₁f h₂f ha).symm.trans (intervalIntegrable_of_odd₀ h₁f h₂f hb)

Premises used: intervalIntegrable_of_odd₀, IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
l l' : Filter ℝ
hfm : StronglyMeasurableAtFilter f l' μ
inst_1 : TendstoIxxClass Ioc l l'
inst_2 : l'.IsMeasurablyGenerated
hμ : μ.FiniteAtFilter l'
c : E
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
u v : ι → ℝ
lt : Filter ι
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)

Tactic:
have := (hf.integrableAtFilter_ae hfm hμ).eventually
  ((hu.Ioc hv).eventually this).and <| (hv.Ioc hu).eventually this

Premises used: IntervalIntegrable, Filter.Tendsto.Ioc, Filter.Eventually.and, Filter.Tendsto.integrableAtFilter_ae, Filter.Tendsto.eventually, MeasureTheory.IntegrableAtFilter.eventually
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
l l' : Filter ℝ
hfm : StronglyMeasurableAtFilter f l' μ
inst_1 : TendstoIxxClass Ioc l l'
inst_2 : l'.IsMeasurablyGenerated
hμ : μ.FiniteAtFilter l'
c : E
hf : Tendsto f l' (𝓝 c)
u v : ι → ℝ
lt : Filter ι
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)

Tactic:
(hf.mono_left inf_le_left).eventually_intervalIntegrable_ae hfm hμ hu hv

Premises used: Filter.Tendsto.eventually_intervalIntegrable_ae, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, 0 ∂μ) 0

Tactic:
simp [intervalIntegral]

Premises used: intervalIntegral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)

Tactic:
simp [intervalIntegral, h]

Premises used: intervalIntegral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..a, f x ∂μ) 0

Tactic:
sub_self _

Premises used: sub_self, intervalIntegral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in b..a, f x ∂μ) (-∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp only [intervalIntegral, neg_sub]

Premises used: neg_sub, intervalIntegral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : b ≤ a
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (-∫ (x : ℝ) in Ioc b a, f x ∂μ)

Tactic:
simp only [integral_symm b, integral_of_le h]

Premises used: intervalIntegral.integral_symm, intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
pos : ∀ (h : a ≤ b), ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ)
neg : ∀ (h : ¬a ≤ b), ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) (-1) (∫ (x : ℝ) in Ι a b, f x ∂μ)
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
simp only [integral_of_le h, uIoc_of_le h, one_smul]

Premises used: one_smul, intervalIntegral.integral_of_le, Set.uIoc_of_le