awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
line3 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
line5 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')| <
    √ε
line7 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| <
    √ε
line2 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| ≤
    √ε
⊢ √ε * (const⁻¹ * ENNReal.toReal ((P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP'))) ≤ √ε
have apply : const⁻¹ * ENNReal.toReal ((P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')) ≤ 1
Tactic: apply mul_le_of_le_one_right (le_of_lt (sqrt_pos_of_pos hε))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
line3 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
line5 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')| <
    √ε
line7 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| <
    √ε
line2 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| ≤
    √ε
⊢ const⁻¹ * ENNReal.toReal ((P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')) ≤ 1
have apply : ENNReal.toReal ((P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')) ≤ P'.real Set.univ
Tactic: apply inv_mul_le_one_of_le₀ (le_max_of_le_right _) (le_of_lt pos_of_measure)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (goal)
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
line3 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
line5 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')| <
    √ε
line7 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| <
    √ε
line2 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| ≤
    √ε
line6 :
  |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')| =
    0
have rw : Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
  (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')
Tactic: rw [abs_eq_zero, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
⊢ ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
have rcases : ∀ (C : ℝ) (C₀ : C ≥ 0) (hC : IsBigOWith C l (deriv f) g),
  ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
Tactic: rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
C : ℝ
C₀ : C ≥ 0
hC : IsBigOWith C l (deriv f) g
⊢ ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
have h : ∀ᶠ (x : ℝ × ℝ) in l ×ˢ l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k
Tactic: have h : ∀ᶠ x : ℝ × ℝ in l ×ˢ l,
        ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k :=
      (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
C : ℝ
C₀ : C ≥ 0
hC : IsBigOWith C l (deriv f) g
h : ∀ᶠ (x : ℝ × ℝ) in l ×ˢ l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k
⊢ ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
have rcases : ∀ (s : Set ℝ) (hsl : s ∈ l)
  (hs :
    s ×ˢ s ⊆
      {x : ℝ × ℝ |
        (fun (x : ℝ × ℝ) ↦ ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k) x}),
  ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
Tactic: rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
C : ℝ
C₀ : C ≥ 0
hC : IsBigOWith C l (deriv f) g
h : ∀ᶠ (x : ℝ × ℝ) in l ×ˢ l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k
s : Set ℝ
hsl : s ∈ l
hs :
  s ×ˢ s ⊆
    {x : ℝ × ℝ | (fun (x : ℝ × ℝ) ↦ ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k) x}
⊢ ∃ (C : ℝ) (_ : 0 ≤ C),
    ∃ s ∈ l,
      (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
        (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
          ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖
have hs₁ : ∀ x ∈ s, ∀ y ∈ s, ∀ y_1 ∈ [[x, y]], (DifferentiableAt ℝ f y_1 ∧ ‖deriv f y_1‖ ≤ C * ‖g y_1‖) ∧ y_1 ∈ k
Tactic: simp only [prod_subset_iff, mem_setOf_eq] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
⊢ False
have obtain : ∀ (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‖), False
Tactic: obtain ⟨C, hC₀, s, hsl, hsub, hfd, hg⟩ :
    ∃ (C : ℝ) (_ : 0 ≤ C), ∃ s ∈ l, (∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
      (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
        ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖ := by
    rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
    have h : ∀ᶠ x : ℝ × ℝ in l ×ˢ l,
        ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k :=
      (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
    rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
    simp only [prod_subset_iff, mem_setOf_eq] at hs
    exact ⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz =>
      (hs x hx y hy z hz).1.1, fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
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‖
⊢ False
have hgi₁ : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume
Tactic: replace hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k := by exact hgi.norm.smul C
Cleared hypotheses: hgi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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 ∈ s,
    ∃ d ∈ s,
      (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) <
        ‖f d‖
have rcases : ∀ (c : ℝ) (hc : c ∈ s),
  ∃ c ∈ s,
    ∃ d ∈ s,
      (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) <
        ‖f d‖
Tactic: rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ ∃ c ∈ s,
    ∃ d ∈ s,
      (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) <
        ‖f d‖
have this : ∀ᶠ (x : ℝ) in l,
  (‖f c‖ + @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume k) fun (y : ℝ) ↦ C * ‖g y‖) < ‖f x‖
Tactic: have : ∀ᶠ x in l, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f x‖ :=
      hf.eventually (eventually_gt_atTop _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (goal)
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
⊢ False
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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‖
⊢ False
have hsub₁ : [[c, d]] ⊆ k
Tactic: specialize hsub c hc d hd
Cleared hypotheses: hsub
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ False
have hfd₁ : ∀ z ∈ [[c, d]], DifferentiableAt ℝ f z
Tactic: specialize hfd c hc d hd
Cleared hypotheses: hfd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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
⊢ False
have hg₁ : ∀ 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⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.NonIntegrable (hypothesis)
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‖
⊢ False
have hg_ae : ∀ᵐ (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