awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ℝ → E} (hfc : ContinuousOn f (Icc a b))
    (hfd : DifferentiableOn ℝ f (Ioo a b)) (hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) (hE : CompleteSpace E),
    ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
hgc : ContinuousOn g (Icc a b)
hgd : DifferentiableOn ℝ g (Ioo a b)
hdg : ∀ (t : ℝ) (ht : t ∈ Ioo a b), deriv g t = (↑(deriv f t) : UniformSpace.Completion E)
hgn : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv g t‖ ≤ B t
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
simpa [g, ← dist_eq_norm_sub] using this hgc hgd hgn inferInstance

Premises used: dist_eq_norm_sub, inferInstance
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
rwa : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioc a b))] B
rwa₁ : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))] B
rwa₂ : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioo a b), ‖deriv f x‖ ≤ B x
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ᵐ (x : ℝ), x ∈ Ioo a b → ‖deriv f x‖ ≤ B x
⊢ (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B

Tactic:
rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ioc, measurableSet_Ioo, MeasureTheory.ae_restrict_iff', Filter.EventuallyLE, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
⊢ (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B

Tactic:
have hfB' : (‖deriv f ·‖) ≤ᵐ[volume.restrict (uIoc a b)] B := by
    rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
rw : norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t
hcont : ContinuousOn f (uIcc a b)
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x
hint : IntervalIntegrable (deriv f) volume a b
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
rw [← intervalIntegral.integral_eq_sub_of_hasDeriv_right (f' := deriv f)]

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
apply : ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t
⊢ norm.{u_1} (E := E) (∫ (y : ℝ) in a..b, deriv f y) ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
apply intervalIntegral.norm_integral_le_of_norm_le hab _ hBi

Premises used: intervalIntegral.norm_integral_le_of_norm_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
rwa : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioc a b), ‖deriv f x‖ ≤ B x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (uIoc a b), ‖deriv f x‖ ≤ B x
⊢ ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t

Tactic:
rwa [← ae_restrict_iff' measurableSet_Ioc, ← uIoc_of_le hab]

Premises used: MeasureTheory.ae_restrict_iff', measurableSet_Ioc, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
hcont hcont₁ hcont₂ hcont₃ : ContinuousOn f (Icc a b)
⊢ ContinuousOn f (uIcc a b)

Tactic:
rwa [uIcc_of_le hab]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (deriv f x) (Ioi x) x
⊢ ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (deriv f x) (Ioi x) x

Tactic:
rw [min_eq_left hab, max_eq_right hab]

Premises used: max_eq_right, min_eq_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
t : ℝ
ht : t ∈ Ioo a b
⊢ HasDerivWithinAt f (deriv f t) (Ioi t) t

Tactic:
hfd.hasDerivAt (isOpen_Ioo.mem_nhds ht) |>.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, isOpen_Ioo, IsOpen.mem_nhds, DifferentiableOn.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
t : ℝ
ht : t ∈ Ioo a b
⊢ HasDerivWithinAt f (deriv f t) (Ioi t) t

Tactic:
exact hfd.hasDerivAt (isOpen_Ioo.mem_nhds ht) |>.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, isOpen_Ioo, IsOpen.mem_nhds, DifferentiableOn.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
hint :
  (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f x‖)
    fun (x : ℝ) ↦ ‖B x‖
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
apply hBi.mono_fun (aestronglyMeasurable_deriv _ _)

Premises used: aestronglyMeasurable_deriv, IntervalIntegrable.mono_fun
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f x‖)
    fun (x : ℝ) ↦ ‖B x‖

Tactic:
hfB'.trans <| .of_forall fun _ ↦ le_abs_self _

Premises used: le_abs_self, Filter.Eventually.of_forall, Filter.EventuallyLE.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
f_1 : ℝ → E_1
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun (x : ℝ) ↦ ‖deriv f x‖) ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] B
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ ‖deriv f x‖)
    fun (x : ℝ) ↦ ‖B x‖

Tactic:
exact hfB'.trans <| .of_forall fun _ ↦ le_abs_self _

Premises used: Filter.EventuallyLE.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
⊢ MeasurableSet s

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
⊢ MeasurableSet s

Tactic:
have hsm : MeasurableSet s := by measurability
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
hBi : IntervalIntegrable (ε := ℝ) (s.indicator fun (x : ℝ) ↦ C) volume a b
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, s.indicator (fun (x : ℝ) ↦ C) t

Tactic:
apply norm_sub_le_integral_of_norm_deriv_le_of_le hab hfc hfd

Premises used: norm_sub_le_integral_of_norm_deriv_le_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t

Tactic:
hnorm.mono fun t ht ht_mem ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
hfB :
  ∀ (t : ℝ) (ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C) (ht_mem : t ∈ Ioo a b), ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t

Tactic:
refine hnorm.mono fun t ht ht_mem ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
hfB : t ∈ s → ‖deriv f t‖ ≤ C
hfB₁ : t ∉ s → ‖deriv f t‖ ≤ 0
⊢ ‖deriv f t‖ ≤ s.indicator (fun (x : ℝ) ↦ C) t

Tactic:
apply le_indicator_apply

Premises used: Set.le_indicator_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ t ∈ s → ‖deriv f t‖ ≤ C

Tactic:
fun ht' ↦ ht ht_mem
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ t ∈ s → ‖deriv f t‖ ≤ C

Tactic:
exact fun ht' ↦ ht ht_mem
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
hfB : t ∉ toMeasurable volume {x : ℝ | deriv f x ≠ 0} → deriv f t = 0
⊢ t ∉ s → ‖deriv f t‖ ≤ 0

Tactic:
simp only [s, norm_le_zero_iff]

Premises used: norm_le_zero_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ t ∉ toMeasurable volume {x : ℝ | deriv f x ≠ 0} → deriv f t = 0

Tactic:
not_imp_comm.2 fun h ↦ subset_toMeasurable _ _ h

Premises used: Iff.mpr, deriv, not_imp_comm, setOf, Ne, MeasureTheory.subset_toMeasurable, MeasureTheory.MeasureSpace.volume, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
t : ℝ
ht : t ∈ Ioo a b → ‖deriv f t‖ ≤ C
ht_mem : t ∈ Ioo a b
⊢ t ∉ toMeasurable volume {x : ℝ | deriv f x ≠ 0} → deriv f t = 0

Tactic:
exact not_imp_comm.2 fun h ↦ subset_toMeasurable _ _ h

Premises used: Iff.mpr, not_imp_comm, MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
hBi : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (s.indicator fun (x : ℝ) ↦ C) (Ioo a b) volume
⊢ IntervalIntegrable (ε := ℝ) (s.indicator fun (x : ℝ) ↦ C) volume a b

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab]

Premises used: intervalIntegrable_iff_integrableOn_Ioo_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (s.indicator fun (x : ℝ) ↦ C) (Ioo a b) volume

Tactic:
(integrableOn_const ?_ ?_).indicator hsm

Premises used: MeasureTheory.IntegrableOn.indicator, MeasureTheory.integrableOn_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
hBi : Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo a b) : ENNReal) (⊤ : ENNReal)
hBi₁ : ‖C‖ₑ ≠ ⊤
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (s.indicator fun (x : ℝ) ↦ C) (Ioo a b) volume

Tactic:
refine (integrableOn_const ?_ ?_).indicator hsm

Premises used: MeasureTheory.IntegrableOn.indicator, MeasureTheory.integrableOn_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo a b) : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ‖C‖ₑ ≠ ⊤

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
rw :
  C * Measure.real (m := Real.measurableSpace) volume (s ∩ Ioo a b) =
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}
⊢ ∫ (t : ℝ) in a..b, s.indicator (fun (x : ℝ) ↦ C) t =
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}

Tactic:
rw [intervalIntegral.integral_of_le hab, Measure.restrict_congr_set Ioo_ae_eq_Ioc.symm,
        integral_indicator hsm, Measure.restrict_restrict hsm,
        setIntegral_const, smul_eq_mul, mul_comm]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Measure.restrict_restrict, intervalIntegral.integral_of_le, MeasureTheory.Ioo_ae_eq_Ioc, mul_comm, smul_eq_mul, Filter.EventuallyEq.symm, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
simp :
  C * ENNReal.toReal ((volume : (a : Set ℝ) → ENNReal) ({x : ℝ | deriv f x ≠ 0} ∩ Ioo a b)) =
    C * ENNReal.toReal ((volume : (a : Set ℝ) → ENNReal) {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0})
⊢ C * Measure.real (m := Real.measurableSpace) volume (s ∩ Ioo a b) =
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}

Tactic:
simp only [s, Measure.real,
        Measure.measure_toMeasurable_inter_of_sFinite measurableSet_Ioo]

Premises used: MeasureTheory.Measure.real, MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite, measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x : ℝ | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ C * ENNReal.toReal ((volume : (a : Set ℝ) → ENNReal) ({x : ℝ | deriv f x ≠ 0} ∩ Ioo a b)) =
    C * ENNReal.toReal ((volume : (a : Set ℝ) → ENNReal) {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0})

Tactic:
simp only [inter_def, mem_setOf_eq, and_comm]

Premises used: Set.mem_setOf_eq, and_comm, Set.inter_def