awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
h :
  ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x) (hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x)
    (hx₃ : x ∈ uIoc a b), deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x

Tactic:
filter_upwards [hf.ae_differentiableAt, hg.ae_differentiableAt] with x hx₁ hx₂ hx₃

Premises used: AbsolutelyContinuousOnInterval.ae_differentiableAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
⊢ x ∈ uIcc a b

Tactic:
grind [uIcc, uIoc]

Premises used: Set.uIoc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
⊢ x ∈ uIcc a b

Tactic:
have hx₄ : x ∈ uIcc a b := by grind [uIcc, uIoc]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
hx₄ : x ∈ uIcc a b
⊢ HasDerivAt (f * g) (deriv f x * g x + f x * deriv g x) x

Tactic:
have hx₅ := (hx₁ hx₄).hasDerivAt.mul (hx₂ hx₄).hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
hx₄ : x ∈ uIcc a b
hx₅ : HasDerivAt (f * g) (deriv f x * g x + f x * deriv g x) x
⊢ deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x

Tactic:
hx₅.deriv.symm

Premises used: HasDerivAt.deriv, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableAt ℝ f x
hx₂ : x ∈ uIcc a b → DifferentiableAt ℝ g x
hx₃ : x ∈ uIoc a b
hx₄ : x ∈ uIcc a b
hx₅ : HasDerivAt (f * g) (deriv f x * g x + f x * deriv g x) x
⊢ deriv f x * g x + f x * deriv g x = deriv (fun (i : ℝ) ↦ f i * g i) x

Tactic:
exact hx₅.deriv.symm

Premises used: HasDerivAt.deriv, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x * deriv g x)
    (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x)
hf₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x + f x * deriv g x) volume a b
hg₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x) volume a b
⊢ ∫ (x : ℝ) in a..b, f x * deriv g x = f b * g b - f a * g a - ∫ (x : ℝ) in a..b, deriv f x * g x

Tactic:
rw [← AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub hf hg,
      ← intervalIntegral.integral_sub]

Premises used: AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub, intervalIntegral.integral_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, f x * deriv g x)
    (∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x - deriv f x * g x)

Tactic:
simp_rw [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x + f x * deriv g x) volume a b

Tactic:
(hf.intervalIntegrable_deriv.mul_continuousOn hg.continuousOn).add
      (hg.intervalIntegrable_deriv.continuousOn_mul hf.continuousOn)

Premises used: IntervalIntegrable.mul_continuousOn, IntervalIntegrable.continuousOn_mul, IntervalIntegrable.add, AbsolutelyContinuousOnInterval.continuousOn, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x + f x * deriv g x) volume a b

Tactic:
exact (hf.intervalIntegrable_deriv.mul_continuousOn hg.continuousOn).add
      (hg.intervalIntegrable_deriv.continuousOn_mul hf.continuousOn)

Premises used: IntervalIntegrable.mul_continuousOn, IntervalIntegrable.continuousOn_mul, IntervalIntegrable.add, AbsolutelyContinuousOnInterval.continuousOn, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x) volume a b

Tactic:
hf.intervalIntegrable_deriv.mul_continuousOn hg.continuousOn

Premises used: IntervalIntegrable.mul_continuousOn, AbsolutelyContinuousOnInterval.continuousOn, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
Goal:
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ deriv f x * g x) volume a b

Tactic:
exact hf.intervalIntegrable_deriv.mul_continuousOn hg.continuousOn

Premises used: IntervalIntegrable.mul_continuousOn, AbsolutelyContinuousOnInterval.continuousOn, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
rw : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b ∪ Ioc b a) μ
rw₁ : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ
rw₂ rw₃ :
  IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ ↔ IntegrableOn f (Ioc a b) μ ∧ IntegrableOn f (Ioc b a) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ

Tactic:
rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]

Premises used: MeasureTheory.integrableOn_union, IntervalIntegrable, Set.uIoc_eq_union
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ IntegrableOn f (Ι a b) μ

Tactic:
intervalIntegrable_iff.mp h

Premises used: intervalIntegrable_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
rw : IntegrableOn f (Ι a b) μ ↔ IntervalIntegrable g μ a b
rw₁ : IntegrableOn g (Ι a b) μ ↔ IntervalIntegrable g μ a b
rw₂ rw₃ : IntegrableOn g (Ι a b) μ ↔ IntegrableOn g (Ι a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b

Tactic:
rw [intervalIntegrable_iff, integrableOn_congr_fun_ae h, intervalIntegrable_iff]

Premises used: intervalIntegrable_iff, MeasureTheory.integrableOn_congr_fun_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
hf : IntervalIntegrable f μ a b
h : f =ᶠ[ae (μ.restrict (Ι a b))] g
rwa rwa₁ rwa₂ rwa₃ : IntervalIntegrable f μ a b
⊢ IntervalIntegrable g μ a b

Tactic:
rwa [← intervalIntegrable_congr_ae h]

Premises used: intervalIntegrable_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : EqOn f g (Ι a b)
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b

Tactic:
intervalIntegrable_congr_ae <| (ae_restrict_mem measurableSet_uIoc).mono h

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_uIoc, Filter.Eventually.mono, intervalIntegrable_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
inst_3 : NoAtoms μ
h : f =ᶠ[codiscreteWithin (Ι a b)] g
hf : IntervalIntegrable f μ a b
⊢ IntervalIntegrable g μ a b

Tactic:
hf.congr_ae (ae_restrict_le_codiscreteWithin measurableSet_Ioc h)

Premises used: ae_restrict_le_codiscreteWithin, IntervalIntegrable.congr_ae, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
inst_3 : NoAtoms μ
h : f =ᶠ[codiscreteWithin (Ι a b)] g
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b

Tactic:
⟨(IntervalIntegrable.congr_codiscreteWithin h ·),
    (IntervalIntegrable.congr_codiscreteWithin h.symm ·)⟩

Premises used: IntervalIntegrable.congr_codiscreteWithin, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Ioc a b) μ
rw₁ rw₂ : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ

Tactic:
rw [intervalIntegrable_iff, uIoc_of_le hab]

Premises used: intervalIntegrable_iff, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f [[a, b]] μ
rw₁ : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
rw₂ : IntegrableOn f (Ioc (min a b) (max a b)) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
rw₃ rw₄ : IntegrableOn f (Ioc (min a b) (max a b)) μ ↔ IntegrableOn f (Ioc (min a b) (max a b)) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ

Tactic:
rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc h]

Premises used: intervalIntegrable_iff, Set.Icc_min_max, Set.uIoc, integrableOn_Icc_iff_integrableOn_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Icc a b) μ
rw₁ rw₂ : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioc a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc ha]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, integrableOn_Icc_iff_integrableOn_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
rw₁ rw₂ : IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab ha,
    integrableOn_Icc_iff_integrableOn_Ico hb]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, integrableOn_Icc_iff_integrableOn_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
rw₁ rw₂ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab ha,
    integrableOn_Icc_iff_integrableOn_Ioo ha hb]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, integrableOn_Icc_iff_integrableOn_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
hf : Integrable f μ
⊢ IntervalIntegrable f μ a b

Tactic:
⟨hf.integrableOn, hf.integrableOn⟩

Premises used: IntervalIntegrable, And.intro, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
hf : IntegrableOn f [[a, b]] μ
⊢ IntervalIntegrable f μ a b

Tactic:
⟨hf.mono_set (Ioc_subset_Icc_self.trans Icc_subset_uIcc),
    hf.mono_set (Ioc_subset_Icc_self.trans Icc_subset_uIcc')⟩

Premises used: IntervalIntegrable, Set.Icc_subset_uIcc, Set.Ioc_subset_Icc_self, HasSubset.Subset.trans, MeasureTheory.IntegrableOn.mono_set, And.intro, Set.Icc_subset_uIcc'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
a b : ℝ
μ : Measure ℝ
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ c) μ a b ↔
    c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [intervalIntegrable_iff, integrableOn_const_iff hc]

Premises used: intervalIntegrable_iff, MeasureTheory.integrableOn_const_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
inst_1 : IsLocallyFiniteMeasure μ
c : E
hc : ‖c‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ c) μ a b

Tactic:
intervalIntegrable_const_iff hc |>.2 <| Or.inr measure_Ioc_lt_top

Premises used: Iff.mpr, intervalIntegrable_const_iff, measure_Ioc_lt_top, Or.inr
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
⊢ enorm.{u_5} (E := E) NegZeroClass.toZero.1 ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ IntervalIntegrable f μ b a

Tactic:
h.symm

Premises used: IntervalIntegrable, And.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntervalIntegrable f μ b a

Tactic:
⟨.symm, .symm⟩

Premises used: IntervalIntegrable.symm, Iff.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a : ℝ
μ : Measure ℝ
left right : IntegrableOn f (Ioc a a) μ
⊢ IntervalIntegrable f μ a a

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a : ℝ
μ : Measure ℝ
⊢ IntegrableOn f (Ioc a a) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a b c : ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ IntervalIntegrable f μ a c

Tactic:
⟨(hab.1.union hbc.1).mono_set Ioc_subset_Ioc_union_Ioc,
    (hbc.2.union hab.2).mono_set Ioc_subset_Ioc_union_Ioc⟩

Premises used: IntervalIntegrable, Set.Ioc_subset_Ioc_union_Ioc, MeasureTheory.IntegrableOn.union, MeasureTheory.IntegrableOn.mono_set, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b c : ℝ
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
h : b ∈ [[a, c]]
⊢ IntervalIntegrable f μ a c ↔ IntervalIntegrable f μ a b ∧ IntervalIntegrable f μ b c

Tactic:
simp only [intervalIntegrable_iff, ← integrableOn_union, uIoc_union_uIoc h]

Premises used: intervalIntegrable_iff, MeasureTheory.integrableOn_union, Set.uIoc_union_uIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))
revert : ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)
⊢ IntervalIntegrable f μ (a m) (a n)

Tactic:
revert hint
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)

Tactic:
Nat.le_induction ?_ ?_ n hmn

Premises used: Nat.le_induction
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
refine_1 : ∀ (hint : ∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a m)
refine_2 :
  ∀ (n : ℕ) (hmn : m ≤ n),
    (∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)) →
      ∀ (hint : ∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a (n + 1))
⊢ ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)

Tactic:
refine Nat.le_induction ?_ ?_ n hmn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (hint : ∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a m)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a p)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)

Tactic:
simp [hp]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a p)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a (p + 1))

Tactic:
exact (IH fun k hk => h k (Ico_subset_Ico_right p.le_succ hk)).trans (h p (by simp [hp]))

Premises used: Nat.le_succ, IntervalIntegrable.trans, Set.Ico_subset_Ico_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a 0) (a n)

Tactic:
trans_iterate_Ico bot_le fun k hk => hint k hk.2

Premises used: IntervalIntegrable.trans_iterate_Ico, And.right, bot_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
h : IntervalIntegrable f μ a b
⊢ IntervalIntegrable (-f) μ a b

Tactic:
⟨h.1.neg, h.2.neg⟩

Premises used: IntervalIntegrable, And.right, And.left, And.intro, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ IntervalIntegrable (ε := ℝ≥0∞) (fun (x : ℝ) ↦ ‖f x‖ₑ) μ a b

Tactic:
⟨h.1.enorm, h.2.enorm⟩

Premises used: IntervalIntegrable, And.right, And.left, MeasureTheory.Integrable.enorm, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
h : IntervalIntegrable f μ a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ a b

Tactic:
⟨h.1.norm, h.2.norm⟩

Premises used: IntervalIntegrable, And.right, And.left, And.intro, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
inst_2 : PseudoMetrizableSpace ε
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
simp_rw : IntegrableOn (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) (Ι a b) μ ↔ IntegrableOn f (Ι a b) μ
simp_rw₁ : Integrable (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))
⊢ IntervalIntegrable (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) μ a b ↔ IntervalIntegrable f μ a b

Tactic:
simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_enorm_iff hf]

Premises used: intervalIntegrable_iff, MeasureTheory.IntegrableOn, MeasureTheory.integrable_enorm_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
simp_rw : IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) (Ι a b) μ ↔ IntegrableOn f (Ι a b) μ
simp_rw₁ : Integrable (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b

Tactic:
simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_norm_iff hf]

Premises used: intervalIntegrable_iff, MeasureTheory.IntegrableOn, MeasureTheory.integrable_norm_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
μ : Measure ℝ
f : ℝ → ℝ
h : IntervalIntegrable f μ a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |f x|) μ a b

Tactic:
h.norm

Premises used: IntervalIntegrable.norm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b c d : ℝ
μ ν : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f ν a b
h1 : [[c, d]] ⊆ [[a, b]]
h2 : μ ≤ ν
⊢ IntervalIntegrable f μ c d

Tactic:
intervalIntegrable_iff.mpr <| hf.def'.mono (uIoc_subset_uIoc_of_uIcc_subset_uIcc h1) h2

Premises used: Iff.mpr, intervalIntegrable_iff, Set.uIoc_subset_uIoc_of_uIcc_subset_uIcc, IntervalIntegrable.def', MeasureTheory.IntegrableOn.mono