awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this_1 :
  ‖HSub.hSub (α := UniformSpace.Completion E) (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) b)
        (((⇑g : (a : E) → UniformSpace.Completion E) ∘ f) a)‖ₑ =
    ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
this : fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) = g.toContinuousLinearMap
⊢ enorm (E := UniformSpace.Completion E)
      ((fderiv ℝ (⇑g : (a : E) → UniformSpace.Completion E) (f x) : (a : E) → UniformSpace.Completion E) (deriv f x) :
        UniformSpace.Completion E) ≤
    ‖deriv f x‖ₑ

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
apply : ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ = ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ
⊢ ‖f b - f a‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ

Tactic:
apply (enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc h hab).trans_eq

Premises used: LE.le.trans_eq, enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h₁ :
  (ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
    fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
⊢ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ = ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h₁ :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
    fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
    fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ

Tactic:
rw [← restrict_Ioo_eq_restrict_Icc]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
    fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ

Tactic:
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx

Premises used: measurableSet_Ioo, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
x : ℝ
hx : x ∈ Ioo a b
h₁ h₂ : ‖deriv f x‖ₑ = ‖deriv f x‖ₑ
⊢ ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ

Tactic:
rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]

Premises used: And.right, And.left, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
⊢ MonotoneOn (β := ℝ) (fun (x : ℝ) ↦ max a (min x b)) univ

Tactic:
grind [MonotoneOn]

Premises used: MonotoneOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
⊢ MapsTo (fun (x : ℝ) ↦ max a (min x b)) univ (Icc a b)

Tactic:
grind [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
⊢ Monotone g

Tactic:
have hg : Monotone g := monotoneOn_univ.mp <| hf.comp (by grind [MonotoneOn]) (by grind [MapsTo])
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
⊢ EqOn f g (Ioo a b)

Tactic:
grind [EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
⊢ EqOn f g (Ioo a b)

Tactic:
have hfg : EqOn f g (Ioo a b) := by grind [EqOn]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn f g (Ioo a b)
⊢ EqOn (deriv f) (deriv g) (Ioo a b)

Tactic:
replace hfg := hfg.deriv isOpen_Ioo
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
⊢ ∀ᵐ (x : ℝ), x ≠ a

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
⊢ ∀ᵐ (x : ℝ), x ≠ a

Tactic:
have h₁ : ∀ᵐ x, x ≠ a := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ≠ b

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ≠ b

Tactic:
have h₂ : ∀ᵐ x, x ≠ b := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
n : ℕ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ slope g x (x + (↑n : ℝ)⁻¹)) volume a b

Tactic:
have := hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegrable_slope hab (by simp)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
n : ℕ
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ slope g x (x + (↑n : ℝ)⁻¹)) volume a b
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))

Tactic:
intervalIntegrable_iff_integrableOn_Icc_of_le hab |>.mp this

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, MeasureTheory.IntegrableOn, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
n : ℕ
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ slope g x (x + (↑n : ℝ)⁻¹)) volume a b
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))

Tactic:
exact intervalIntegrable_iff_integrableOn_Icc_of_le hab |>.mp this

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
⊢ ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))

Tactic:
have G_integrable (n : ℕ) : Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b)) := by
    have := hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegrable_slope hab (by simp)
    exact intervalIntegrable_iff_integrableOn_Icc_of_le hab |>.mp this
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)

Tactic:
⟨fun n x ↦ G (n : ℝ)⁻¹ x, ?_, fun n ↦ G_integrable n |>.aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Nat.cast, Inv.inv, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
refine_1 :
  ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b),
    Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
refine_2 :
  liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x)) atTop ≤
    ENNReal.ofReal (f b - f a)
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)

Tactic:
refine ⟨fun n x ↦ G (n : ℝ)⁻¹ x, ?_, fun n ↦ G_integrable n |>.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
⊢ MeasurableSet (Icc a b)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
refine_1 :
  ∀ᵐ (x : ℝ), x ∈ Icc a b → Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b),
    Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))

Tactic:
rw [MeasureTheory.ae_restrict_iff' (by measurability)]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
h :
  ∀ (x : ℝ) (hx₁ : DifferentiableAt ℝ g x) (hx₂ : x ≠ a) (hx₃ : x ≠ b) (hx₄ : x ∈ Icc a b),
    Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv f x))
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))

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

Premises used: Monotone.ae_differentiableAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ x ∈ Ioo a b

Tactic:
grind [Icc_diff_both]

Premises used: Set.Icc_diff_both
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
h : Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv g x))
⊢ Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv f x))

Tactic:
rw [hfg (by grind [Icc_diff_both])]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ Tendsto (fun (x_1 : ℕ) ↦ x + (↑x_1 : ℝ)⁻¹) atTop (𝓝 (x + 0))

Tactic:
tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ))

Premises used: tendsto_const_nhds, Filter.Tendsto.add, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
h : x = x + 0
⊢ Tendsto (fun (n : ℕ) ↦ x + (↑n : ℝ)⁻¹) atTop (𝓝 x)

Tactic:
convert! tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ))

Premises used: tendsto_const_nhds, Filter.Tendsto.add, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ x = x + 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set ℝ) {x}ᶜ (x + (↑x_1 : ℝ)⁻¹)

Tactic:
simp [eventually_ne_atTop 0]

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv g x))

Tactic:
exact hx₁.hasDerivAt.tendsto_slope.comp <|
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      (by convert! tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ)); simp)
      (by simp [eventually_ne_atTop 0])

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.tendsto_slope, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
h :
  ∀ᶠ (a_1 : ℕ) in atTop,
    ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) a_1 x) =
      ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
          G (↑a_1 : ℝ)⁻¹ x)
⊢ Eq (α := ENNReal)
    (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x)) atTop)
    (liminf
      (fun (n : ℕ) ↦
        ENNReal.ofReal
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
            G (↑n : ℝ)⁻¹ x))
      atTop)

Tactic:
apply Filter.liminf_congr

Premises used: Filter.liminf_congr
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
h :
  ∀ (n : ℕ),
    ∫⁻ (x : ℝ) in Icc a b, ‖G (↑n : ℝ)⁻¹ x‖ₑ =
      ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
          G (↑n : ℝ)⁻¹ x)
⊢ ∀ᶠ (a_1 : ℕ) in atTop,
    ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) a_1 x) =
      ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
          G (↑a_1 : ℝ)⁻¹ x)

Tactic:
filter_upwards with n
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
h :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        ‖G (↑n : ℝ)⁻¹ x‖) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x)
⊢ ∫⁻ (x : ℝ) in Icc a b, ‖G (↑n : ℝ)⁻¹ x‖ₑ =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x)

Tactic:
rw [← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm (G_integrable n)]

Premises used: MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
h : ∀ (y : ℝ), ‖G (↑n : ℝ)⁻¹ y‖ = G (↑n : ℝ)⁻¹ y
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        ‖G (↑n : ℝ)⁻¹ x‖) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x)

Tactic:
congr with y