awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
this :
  ∀ᶠ (x : ℝ) in l,
    (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) <
      ‖f x‖
⊢ ∃ c ∈ s,
    ∃ d ∈ s,
      (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) <
        ‖f d‖

Tactic:
exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
obtain :
  ∀ (c : ℝ) (hc : c ∈ s) (d : ℝ) (hd : d ∈ s)
    (hlt :
      (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) <
        ‖f d‖),
    False
⊢ False

Tactic:
obtain ⟨c, hc, d, hd, hlt⟩ : ∃ c ∈ s, ∃ d ∈ s, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f d‖ := by
    rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
    have : ∀ᶠ x in l, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f x‖ :=
      hf.eventually (eventually_gt_atTop _)
    exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hsub : ∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
⊢ [[c, d]] ⊆ k

Tactic:
specialize hsub c hc d hd
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hfd : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
⊢ ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z

Tactic:
specialize hfd c hc d hd
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hg : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
⊢ ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖

Tactic:
replace hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖ :=
    fun z hz => hg c hc d hd z ⟨hz.1.le, hz.2⟩
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖

Tactic:
have hg_ae : ∀ᵐ x ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖ :=
    (ae_restrict_mem measurableSet_uIoc).mono hg
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
⊢ Ι c d ⊆ k

Tactic:
have hsub' : Ι c d ⊆ k := Subset.trans Ioc_subset_Icc_self hsub
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
rw : IntegrableOn (mα := Real.measurableSpace) (deriv f) (Ι c d) volume
⊢ IntervalIntegrable (deriv f) volume c d

Tactic:
rw [intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) (Ι c d) volume

Tactic:
have : IntegrableOn (fun x ↦ C * ‖g x‖) (Ι c d) := IntegrableOn.mono hgi hsub' le_rfl
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) (Ι c d) volume
⊢ IntegrableOn (mα := Real.measurableSpace) (deriv f) (Ι c d) volume

Tactic:
Integrable.mono' this (aestronglyMeasurable_deriv _ _) hg_ae

Premises used: MeasureTheory.Integrable.mono', aestronglyMeasurable_deriv, MeasureTheory.IntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) (Ι c d) volume
⊢ IntegrableOn (mα := Real.measurableSpace) (deriv f) (Ι c d) volume

Tactic:
exact Integrable.mono' this (aestronglyMeasurable_deriv _ _) hg_ae

Premises used: MeasureTheory.Integrable.mono', aestronglyMeasurable_deriv
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
⊢ IntervalIntegrable (deriv f) volume c d

Tactic:
have hfi : IntervalIntegrable (deriv f) volume c d := by
    rw [intervalIntegrable_iff]
    have : IntegrableOn (fun x ↦ C * ‖g x‖) (Ι c d) := IntegrableOn.mono hgi hsub' le_rfl
    exact Integrable.mono' this (aestronglyMeasurable_deriv _ _) hg_ae
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ False

Tactic:
hlt.not_ge (sub_le_iff_le_add'.1 ?_)

Premises used: sub_le_iff_le_add', Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
refine :
  ‖f d‖ - ‖f c‖ ≤ @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖
⊢ False

Tactic:
refine hlt.not_ge (sub_le_iff_le_add'.1 ?_)

Premises used: sub_le_iff_le_add', Iff.mp, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ ‖f d‖ - ‖f c‖ ≤ ‖f d - f c‖

Tactic:
norm_sub_norm_le _ _

Premises used: norm_sub_norm_le
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ ‖f d - f c‖ = norm.{u_1} (E := E) (∫ (x : ℝ) in c..d, deriv f x)

Tactic:
congr_arg _ (integral_deriv_eq_sub hfd hfi).symm

Premises used: intervalIntegral.integral_deriv_eq_sub, congr_arg, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ norm.{u_1} (E := E) (∫ (x : ℝ) in c..d, deriv f x) =
    norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ deriv f x)

Tactic:
norm_integral_eq_norm_integral_uIoc _

Premises used: intervalIntegral.norm_integral_eq_norm_integral_uIoc
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ deriv f x) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ ‖deriv f x‖

Tactic:
norm_integral_le_integral_norm _

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ ‖deriv f x‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ C * ‖g x‖)

Tactic:
setIntegral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg

Premises used: measurableSet_uIoc, IntervalIntegrable.norm, MeasureTheory.IntegrableOn.mono_set, IntervalIntegrable.def', MeasureTheory.setIntegral_mono_on
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : CompleteSpace E
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst_4 : l.NeBot
inst_5 : TendstoIxxClass Icc l l
hl : k ∈ l
hd_1 : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
C : ℝ
hC₀ : 0 ≤ C
s : Set ℝ
hsl : s ∈ l
hgi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
c : ℝ
hc : c ∈ s
d : ℝ
hd : d ∈ s
hlt :
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f d‖
hsub : [[c, d]] ⊆ k
hfd : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖
hg_ae : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖
hsub' : Ι c d ⊆ k
hfi : IntervalIntegrable (deriv f) volume c d
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι c d)) fun (x : ℝ) ↦ C * ‖g x‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (x : ℝ) ↦ C * ‖g x‖)

Tactic:
apply setIntegral_mono_set hgi
        (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE

Premises used: mul_nonneg, MeasureTheory.setIntegral_mono_set, HasSubset.Subset.eventuallyLE, MeasureTheory.ae_of_all, norm_nonneg