awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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')| ≤
    √ε
⊢ Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
    (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')

Tactic:
integral_mulExpNegMulSq_comp_eq hε heq hgA

Premises used: integral_mulExpNegMulSq_comp_eq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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')| ≤
    √ε
⊢ Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
    (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')

Tactic:
exact integral_mulExpNegMulSq_comp_eq hε heq hgA

Premises used: integral_mulExpNegMulSq_comp_eq
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
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

Tactic:
have line4 : |∫ x, mulExpNegMulSq ε (g x) ∂P
      - ∫ x, mulExpNegMulSq ε (g x) ∂P'| = 0 := by
    rw [abs_eq_zero, sub_eq_zero]
    exact integral_mulExpNegMulSq_comp_eq hε heq hgA
-- 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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
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‖
⊢ ∃ (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⟩

Premises used: Asymptotics.IsBigO.exists_nonneg
-- 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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
C : ℝ
C₀ : C ≥ 0
hC : IsBigOWith C l (deriv f) g
⊢ ∀ᶠ (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
-- 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
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
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‖
⊢ ∃ (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⟩

Premises used: Filter.mem_prod_self_iff, Iff.mp
-- 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
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}
⊢ ∀ 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

Premises used: Set.prod_subset_iff, Set.mem_setOf_eq
-- 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
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 : ∀ x ∈ s, ∀ y ∈ s, ∀ y_1 ∈ [[x, y]], (DifferentiableAt ℝ f y_1 ∧ ‖deriv f y_1‖ ≤ C * ‖g y_1‖) ∧ y_1 ∈ 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‖

Tactic:
⟨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⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- 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
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 : ∀ x ∈ s, ∀ y ∈ s, ∀ y_1 ∈ [[x, y]], (DifferentiableAt ℝ f y_1 ∧ ‖deriv f y_1‖ ≤ C * ‖g y_1‖) ∧ y_1 ∈ 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‖

Tactic:
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⟩
-- 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
hgi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g k volume
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
⊢ 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⟩
-- 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
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‖
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume

Tactic:
hgi.norm.smul C

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.IntegrableOn, MeasureTheory.Integrable.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 : ∀ᶠ (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‖
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ C * ‖g x‖) k volume

Tactic:
exact hgi.norm.smul C

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.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 : ∀ᶠ (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‖
⊢ 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
-- 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
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‖
⊢ ∃ 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⟩

Premises used: Filter.nonempty_of_mem
-- 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
⊢ ∀ᶠ (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 _)
-- 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:
⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩

Premises used: Filter.Eventually.and, Exists.imp, Filter.Eventually.exists, And.intro, Exists.intro