awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
x : ℝ
h : x ≠ b
h_1 : x ∈ Ioc a b
⊢ x ∈ Ioo a b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
x : ℝ
h : x ≠ b
h_1 : x ∈ Ioc a b
⊢ deriv f x = ‖deriv f x‖

Tactic:
exact abs_eq_self.mpr (f_deriv_nonneg (by grind)) |>.symm

Premises used: Iff.mpr, Eq.symm, abs_eq_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : BoundedVariationOn f (uIcc a b)
obtain :
  ∀ (p q : ℝ → ℝ) (hp : MonotoneOn p (uIcc a b)) (hq : MonotoneOn q (uIcc a b))
    (hf : BoundedVariationOn (p - q) (uIcc a b)), IntervalIntegrable (deriv (p - q)) volume a b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
obtain ⟨p, q, hp, hq, rfl⟩ := hf.locallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn

Premises used: BoundedVariationOn.locallyBoundedVariationOn, LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
⊢ ∀ᵐ (x : ℝ), x ≠ max a b

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
⊢ ∀ᵐ (x : ℝ), x ≠ max a b

Tactic:
have h₂ : ∀ᵐ x, x ≠ max a b := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
apply : (fun (x : ℝ) ↦ deriv p x - deriv q x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] deriv (p - q)
⊢ IntervalIntegrable (deriv (p - q)) volume a b

Tactic:
apply (hp.intervalIntegrable_deriv.sub hq.intervalIntegrable_deriv).congr_ae

Premises used: MonotoneOn.intervalIntegrable_deriv, IntervalIntegrable.sub, IntervalIntegrable.congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ MeasurableSet (uIoc a b)

Tactic:
simp [uIoc]

Premises used: Set.uIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
rw : ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv p x - deriv q x = deriv (p - q) x
⊢ (fun (x : ℝ) ↦ deriv p x - deriv q x) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (uIoc a b))] deriv (p - q)

Tactic:
rw [Filter.EventuallyEq, MeasureTheory.ae_restrict_iff' (by simp [uIoc])]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
h :
  ∀ (x : ℝ) (hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x)
    (hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x) (hx₃ : x ≠ max a b) (hx₄ : x ∈ uIoc a b),
    deriv p x - deriv q x = deriv (p - q) x
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv p x - deriv q x = deriv (p - q) x

Tactic:
filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem, h₂]
    with x hx₁ hx₂ hx₃ hx₄

Premises used: MonotoneOn.ae_differentiableWithinAt_of_mem
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ uIoc a b
⊢ x ∈ uIcc a b

Tactic:
have hx₅ : x ∈ uIcc a b := Ioc_subset_Icc_self hx₄
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ uIoc a b
hx₅ : x ∈ uIcc a b
⊢ min a b < x ∧ x ≤ max a b

Tactic:
rw [uIoc, mem_Ioc] at hx₄

Premises used: Set.uIoc, Set.mem_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : x ∈ uIoc a b
hx₅ : x ∈ uIcc a b
hx₆ : min a b < x ∧ x ≤ max a b
⊢ x ∈ uIcc a b

Tactic:
rw [uIoc, mem_Ioc] at hx₄

Premises used: Set.uIoc, Set.mem_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ uIcc a b ∈ 𝓝 x

Tactic:
have hx₆ : uIcc a b ∈ 𝓝 x := Icc_mem_nhds hx₄.left (lt_of_le_of_ne hx₄.right hx₃)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
⊢ HasDerivAt p (deriv p x) x

Tactic:
replace hx₁ := (hx₁ hx₅).differentiableAt hx₆ |>.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
hx₁ : HasDerivAt p (deriv p x) x
⊢ HasDerivAt q (deriv q x) x

Tactic:
replace hx₂ := (hx₂ hx₅).differentiableAt hx₆ |>.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
hx₁ : HasDerivAt p (deriv p x) x
hx₂ : HasDerivAt q (deriv q x) x
⊢ deriv p x - deriv q x = deriv (p - q) x

Tactic:
(hx₁.sub hx₂).deriv.symm

Premises used: HasDerivAt.deriv, HasDerivAt.sub, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
hx₁ : HasDerivAt p (deriv p x) x
hx₂ : HasDerivAt q (deriv q x) x
⊢ deriv p x - deriv q x = deriv (p - q) x

Tactic:
exact (hx₁.sub hx₂).deriv.symm

Premises used: HasDerivAt.deriv, HasDerivAt.sub, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
hf.boundedVariationOn.intervalIntegrable_deriv

Premises used: AbsolutelyContinuousOnInterval.boundedVariationOn, BoundedVariationOn.intervalIntegrable_deriv
-- 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
inr :
  ∀
    (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), ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
wlog :
  ∀ {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
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
wlog hE : CompleteSpace E generalizing E

Premises used: CompleteSpace
-- 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
⊢ let g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f;
  g = UniformSpace.Completion.coe' ∘ f

Tactic:
set g : ℝ → UniformSpace.Completion E := (↑) ∘ f with hg
-- 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
⊢ ContinuousOn g (Icc a b)

Tactic:
have hgc : ContinuousOn g (Icc a b) :=
      (UniformSpace.Completion.continuous_coe E).comp_continuousOn hfc
-- 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)
⊢ DifferentiableOn ℝ g (Ioo a b)

Tactic:
have hgd : DifferentiableOn ℝ g (Ioo a b) :=
      UniformSpace.Completion.toComplL.differentiable.comp_differentiableOn hfd
-- 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)
t : ℝ
ht : t ∈ Ioo a b
⊢ HasFDerivAt (𝕜 := ℝ) (⇑UniformSpace.Completion.toComplL : (a : E) → UniformSpace.Completion E)
    UniformSpace.Completion.toComplL (f t)

Tactic:
(UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt, UniformSpace.Completion.toComplL
-- 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)
t : ℝ
ht : t ∈ Ioo a b
⊢ HasFDerivAt (𝕜 := ℝ) (⇑UniformSpace.Completion.toComplL : (a : E) → UniformSpace.Completion E)
    UniformSpace.Completion.toComplL (f t)

Tactic:
exact (UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt, UniformSpace.Completion.toComplL
-- 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)
t : ℝ
ht : t ∈ Ioo a b
⊢ HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)

Tactic:
have : HasFDerivAt (𝕜 := ℝ) (↑) UniformSpace.Completion.toComplL (f t) := by
        rw [← UniformSpace.Completion.coe_toComplL (𝕜 := ℝ)]
        exact (UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt
-- 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_1 :
  ∀ {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)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
⊢ HasDerivAt f (deriv f t) t

Tactic:
have hdft : HasDerivAt f (deriv f t) t := hfd.hasDerivAt <| Ioo_mem_nhds ht.1 ht.2
-- 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_1 :
  ∀ {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)
t : ℝ
ht : t ∈ Ioo a b
this : HasFDerivAt (𝕜 := ℝ) UniformSpace.Completion.coe' UniformSpace.Completion.toComplL (f t)
hdft : HasDerivAt f (deriv f t) t
rw :
  Eq (α := UniformSpace.Completion E) (deriv (UniformSpace.Completion.coe' ∘ f) t)
    (↑(deriv f t) : UniformSpace.Completion E)
rw₁ :
  Eq (α := UniformSpace.Completion E)
    ((UniformSpace.Completion.toComplL : (a : E) → UniformSpace.Completion E) (deriv f t) : UniformSpace.Completion E)
    ((↑(deriv f t) : UniformSpace.Completion E) : UniformSpace.Completion E)
rw₂ rw₃ :
  Eq (α := UniformSpace.Completion E) (↑(deriv f t) : UniformSpace.Completion E)
    (↑(deriv f t) : UniformSpace.Completion E)
⊢ deriv g t = (↑(deriv f t) : UniformSpace.Completion E)

Tactic:
rw [hg, (this.comp_hasDerivAt t hdft).deriv, UniformSpace.Completion.coe_toComplL]

Premises used: HasDerivAt.deriv, HasFDerivAt.comp_hasDerivAt, UniformSpace.Completion.coe_toComplL
-- 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)
⊢ ∀ (t : ℝ) (ht : t ∈ Ioo a b), deriv g t = (↑(deriv f t) : UniformSpace.Completion E)

Tactic:
have hdg t (ht : t ∈ Ioo a b) : deriv g t = deriv f t := by
      have : HasFDerivAt (𝕜 := ℝ) (↑) UniformSpace.Completion.toComplL (f t) := by
        rw [← UniformSpace.Completion.coe_toComplL (𝕜 := ℝ)]
        exact (UniformSpace.Completion.toComplL (E := E) (𝕜 := ℝ)).hasFDerivAt
      have hdft : HasDerivAt f (deriv f t) t := hfd.hasDerivAt <| Ioo_mem_nhds ht.1 ht.2
      rw [hg, (this.comp_hasDerivAt t hdft).deriv, UniformSpace.Completion.coe_toComplL]
-- 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)
t : ℝ
htB : t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
ht : t ∈ Ioo a b
⊢ ‖deriv g t‖ ≤ B t

Tactic:
simpa only [hdg t ht, UniformSpace.Completion.norm_coe] using htB ht

Premises used: UniformSpace.Completion.norm_coe
-- 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)
⊢ ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv g t‖ ≤ B t

Tactic:
have hgn : ∀ᵐ t, t ∈ Ioo a b → ‖deriv g t‖ ≤ B t :=
      hfB.mono fun t htB ht ↦ by
        simpa only [hdg t ht, UniformSpace.Completion.norm_coe] using htB ht