awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
have hBi : Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Ioo a b) : ENNReal) (⊤ : ENNReal)
Tactic: refine (integrableOn_const ?_ ?_).indicator hsm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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)
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (s.indicator fun (x : ℝ) ↦ C) (Ioo a b) volume
have hBi₁ : ‖C‖ₑ ≠ ⊤
Tactic: refine (integrableOn_const ?_ ?_).indicator hsm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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 : ℝ) 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}
have 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}
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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 * 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}
have 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})
Tactic: simp only [s, Measure.real,
        Measure.measure_toMeasurable_inter_of_sFinite measurableSet_Ioo]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ ‖f b - f a‖ ≤
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}
have b₁ : ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, s.indicator (fun (x : ℝ) ↦ C) t
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ ‖f b - f a‖ ≤
    C * Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ℝ | x ∈ Ioo a b ∧ deriv f x ≠ 0}
have 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}
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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)
have refine_1 : ContinuousOn (X := ℝ) (Y := E) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)
Tactic: refine hfc.comp ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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)
⊢ ContinuousOn g (Icc 0 1)
have refine_2 : MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) (segment ℝ a b)
Tactic: refine hfc.comp ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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)
⊢ ‖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}
have hgc : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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
have 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
Tactic: have := (hfd t ht).hasLineDerivAt.scomp_of_eq (𝕜 := ℝ) t ((hasDerivAt_id t).sub_const t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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)
⊢ ‖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}
have hdg : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖ ≤
    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}
have h : ‖f b - f a‖ = ‖g 1 - g 0‖
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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‖
⊢ ‖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}
have 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}
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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}
⊢ 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}
have 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
Tactic: congr 2 with t
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ ‖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}
have suffices : ‖g 1 - g 0‖ ≤
  C *
    Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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
⊢ ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
have hfd₁ : DifferentiableOn ℝ g (Ioo 0 1)
Tactic: apply norm_sub_le_mul_volume_of_norm_deriv_le_of_le zero_le_one hgc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (goal)
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)
⊢ ‖g 1 - g 0‖ ≤
    C *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ | Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ deriv g t ≠ 0}
have hnorm : ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → ‖deriv g t‖ ≤ C
Tactic: apply norm_sub_le_mul_volume_of_norm_deriv_le_of_le zero_le_one hgc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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
⊢ ‖f b - f a‖ ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}
have hmem_s : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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)
⊢ ‖f b - f a‖ ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}
have hC₀ : 0 ≤ C
Tactic: have hC₀ : 0 ≤ C := (norm_nonneg _).trans <| hC _ <| hmem_s (1 / 2) (by norm_num)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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)
hC₀ : 0 ≤ C
⊢ ‖f b - f a‖ ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}
have hfc : ContinuousOn f (segment ℝ a b)
Tactic: have hfc : ContinuousOn f (segment ℝ a b) :=
    hf.continuousOn.mono <| segment_subset_closure_openSegment.trans <| closure_mono hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral (hypothesis)
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)
hC₀ : 0 ≤ C
hfc : ContinuousOn f (segment ℝ a b)
⊢ ‖f b - f a‖ ≤
    C * ‖b - a‖ *
      Measure.real (α := ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        {t : ℝ |
          Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧ Ne (α := E →L[ℝ] F) (fderiv ℝ f ((lineMap a b : (a : ℝ) → E) t)) 0}
have hfd : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) t → LineDifferentiableAt ℝ f ((lineMap a b : (a : ℝ) → E) t) (b - a)
Tactic: have hfd : ∀ t ∈ Ioo (0 : ℝ) 1, LineDifferentiableAt ℝ f (lineMap a b t) (b - a) := fun t ht ↦
    (hf.differentiableAt hs <| hmem_s t ht).lineDifferentiableAt