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 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
b₁ : ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, s.indicator (fun (x : ℝ) ↦ C) t
b₂ :
  ∫ (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}
⊢ ‖f b - f a‖ ≤
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}

Tactic:
calc
    ‖f b - f a‖ ≤ ∫ t in a..b, indicator s (fun _ ↦ C) t := by
      apply norm_sub_le_integral_of_norm_deriv_le_of_le hab hfc hfd
      · refine hnorm.mono fun t ht ht_mem ↦ ?_
        apply le_indicator_apply
        · exact fun ht' ↦ ht ht_mem
        · simp only [s, norm_le_zero_iff]
          exact not_imp_comm.2 fun h ↦ subset_toMeasurable _ _ h
      · rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab]
        refine (integrableOn_const ?_ ?_).indicator hsm <;> simp
    _ = C * volume.real {x ∈ Ioo a b | deriv f x ≠ 0} := by
      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]
      simp only [s, Measure.real,
        Measure.measure_toMeasurable_inter_of_sFinite measurableSet_Ioo]
      simp only [inter_def, mem_setOf_eq, and_comm]

Premises used: deriv, setOf, MeasureTheory.Measure.real, Membership.mem, Ne, And, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Set.Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
⊢ ContinuousOn g (Icc 0 1)

Tactic:
hfc.comp ?_ ?_

Premises used: ContinuousOn.comp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
refine_1 : ContinuousOn (X := ℝ) (Y := E) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)
refine_2 : MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) (segment ℝ a b)
⊢ ContinuousOn g (Icc 0 1)

Tactic:
refine hfc.comp ?_ ?_

Premises used: ContinuousOn.comp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
⊢ ContinuousOn (X := ℝ) (Y := E) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)

Tactic:
AffineMap.lineMap_continuous.continuousOn

Premises used: Continuous.continuousOn, AffineMap.lineMap_continuous
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
⊢ ContinuousOn (X := ℝ) (Y := E) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)

Tactic:
exact AffineMap.lineMap_continuous.continuousOn

Premises used: Continuous.continuousOn, AffineMap.lineMap_continuous
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
⊢ MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) (segment ℝ a b)

Tactic:
simp [segment_eq_image_lineMap, mapsTo_image]

Premises used: Set.mapsTo_image, segment_eq_image_lineMap
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
⊢ ContinuousOn g (Icc 0 1)

Tactic:
have hgc : ContinuousOn g (Icc 0 1) := by
    refine hfc.comp ?_ ?_
    · exact AffineMap.lineMap_continuous.continuousOn
    · simp [segment_eq_image_lineMap, mapsTo_image]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ ∀ (hy : 0 = _root_.id t - t),
    HasDerivAt
      ((fun (t_1 : ℝ) ↦ f (HAdd.hAdd (α := E) ((lineMap a b : (a : ℝ) → E) t : E) (t_1 • (b - a)))) ∘ fun (x : ℝ) ↦
        _root_.id x - t)
      (HSMul.hSMul (α := ℝ) 1 (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a))) t

Tactic:
have := (hfd t ht).hasLineDerivAt.scomp_of_eq (𝕜 := ℝ) t ((hasDerivAt_id t).sub_const t)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
this :
  ∀ (hy : 0 = _root_.id t - t),
    HasDerivAt
      ((fun (t_1 : ℝ) ↦ f (HAdd.hAdd (α := E) ((lineMap a b : (a : ℝ) → E) t : E) (t_1 • (b - a)))) ∘ fun (x : ℝ) ↦
        _root_.id x - t)
      (HSMul.hSMul (α := ℝ) 1 (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a))) t
⊢ HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t

Tactic:
simpa [g, lineMap_apply_module', Function.comp_def, sub_smul, add_comm _ a] using this

Premises used: sub_smul, AffineMap.lineMap_apply_module', add_comm, Function.comp_def
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
⊢ ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t

Tactic:
have hdg (t : ℝ) (ht : t ∈ Ioo 0 1) : HasDerivAt g (lineDeriv ℝ f (lineMap a b t) (b - a)) t := by
    have := (hfd t ht).hasLineDerivAt.scomp_of_eq (𝕜 := ℝ) t ((hasDerivAt_id t).sub_const t)
    simpa [g, lineMap_apply_module', Function.comp_def, sub_smul, add_comm _ a] using this
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
this :
  ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
⊢ ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}

Tactic:
this
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
this :
  ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
h : ‖f b - f a‖ = ‖g 1 - g 0‖
h₁ :
  C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0} =
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
⊢ ‖f b - f a‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0}

Tactic:
convert! this using 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
this :
  ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
⊢ ‖f b - f a‖ = ‖g 1 - g 0‖

Tactic:
simp [g]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
this :
  ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
h :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ)
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0}
        t ↔
      Membership.mem (γ := Set ℝ) {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0} t
⊢ C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0} =
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}

Tactic:
congr 2 with t
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
this :
  ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
t : ℝ
⊢ Membership.mem (γ := Set ℝ)
      {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0} t ↔
    Membership.mem (γ := Set ℝ) {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0} t

Tactic:
simp +contextual [(hdg _ _).deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
suffices :
  ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
⊢ ‖f b - f a‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a) ≠ 0}

Tactic:
suffices ‖g 1 - g 0‖ ≤ C * volume.real {t ∈ Ioo 0 1 | deriv g t ≠ 0} by
    convert! this using 1
    · simp [g]
    · congr 2 with t
      simp +contextual [(hdg _ _).deriv]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
hfd₁ : DifferentiableOn ℝ g (Ioo 0 1)
hnorm : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖deriv g t‖ ≤ C
⊢ ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}

Tactic:
apply norm_sub_le_mul_volume_of_norm_deriv_le_of_le zero_le_one hgc

Premises used: norm_sub_le_mul_volume_of_norm_deriv_le_of_le, zero_le_one
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
⊢ DifferentiableOn ℝ g (Ioo 0 1)

Tactic:
fun t ht ↦ (hdg t ht).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
⊢ DifferentiableOn ℝ g (Ioo 0 1)

Tactic:
exact fun t ht ↦ (hdg t ht).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
ht_mem : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
⊢ ‖deriv g t‖ ≤ C

Tactic:
simpa only [(hdg t ht_mem).deriv] using ht ht_mem

Premises used: HasDerivAt.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
hfc : ContinuousOn f (segment ℝ a b)
hfd :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
hf' : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)‖ ≤ C
g : ℝ → F := fun (t : ℝ) ↦ f ((lineMap a b : (a : ℝ) → E) t)
hgc : ContinuousOn g (Icc 0 1)
hdg :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t),
    HasDerivAt g (lineDeriv ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)) t
⊢ ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖deriv g t‖ ≤ C

Tactic:
exact hf'.mono fun t ht ht_mem ↦ by simpa only [(hdg t ht_mem).deriv] using ht ht_mem

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
⊢ ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)

Tactic:
have hmem_s : ∀ t ∈ Ioo (0 : ℝ) 1, lineMap a b t ∈ s := fun t ht ↦
    hab <| lineMap_mem_openSegment _ a b ht
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a b : E
C : ℝ
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DiffContOnCl ℝ f s
hab : openSegment ℝ a b ⊆ s
hC : ∀ x ∈ s, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C
hmem_s :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → Membership.mem (α := E) s ((lineMap a b : (a : ℝ) → E) t : E)
⊢ Membership.mem (γ := Set ℝ) (Ioo 0 1) (1 / 2)

Tactic:
norm_num