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
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntegrableOn (mα := Real.measurableSpace) g [[a, b]] volume

Tactic:
not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter _ hl hd hf hfg

Premises used: not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter
-- 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
f : ℝ → E
g : ℝ → F
a b : ℝ
l : Filter ℝ
inst_3 : l.NeBot
inst_4 : TendstoIxxClass Icc l l
hl : [[a, b]] ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntegrableOn (mα := Real.measurableSpace) g [[a, b]] volume

Tactic:
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter _ hl hd hf hfg

Premises used: not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
inl : ∀ (hlt : min a b < c), ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
inr : ∀ (hlt : c < max a b), ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt

Premises used: Iff.mpr, LT.lt.gt_or_lt, min_lt_max
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩

Premises used: nhdsWithin, inferInstance, And.intro, Exists.intro, inf_le_left, Set.Iio
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
inl : [[a, b]] \ {c} ∈ 𝓝[<] c
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
refine ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
inl : [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c
⊢ [[a, b]] \ {c} ∈ 𝓝[<] c

Tactic:
rw [← Iic_diff_right]

Premises used: Set.Iic_diff_right
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c

Tactic:
diff_mem_nhdsWithin_diff (Icc_mem_nhdsLE_of_mem ⟨hlt, hc.2⟩) _

Premises used: Set.Mem, setOf, And.right, diff_mem_nhdsWithin_diff, And.intro, Set.uIcc, Icc_mem_nhdsLE_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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : min a b < c
⊢ [[a, b]] \ {c} ∈ 𝓝[Iic c \ {c}] c

Tactic:
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsLE_of_mem ⟨hlt, hc.2⟩) _

Premises used: And.right, diff_mem_nhdsWithin_diff, And.intro, Icc_mem_nhdsLE_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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, ?_⟩

Premises used: Set.Ioi, nhdsWithin, inferInstance, And.intro, Exists.intro, inf_le_left
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
inr : [[a, b]] \ {c} ∈ 𝓝[>] c
⊢ ∃ (l : Filter ℝ), TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l

Tactic:
refine ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, ?_⟩
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
inr : [[a, b]] \ {c} ∈ 𝓝[Ici c \ {c}] c
⊢ [[a, b]] \ {c} ∈ 𝓝[>] c

Tactic:
rw [← Ici_diff_left]

Premises used: Set.Ici_diff_left
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[Ici c \ {c}] c

Tactic:
diff_mem_nhdsWithin_diff (Icc_mem_nhdsGE_of_mem ⟨hc.1, hlt⟩) _

Premises used: Set.Mem, setOf, Icc_mem_nhdsGE_of_mem, And.left, diff_mem_nhdsWithin_diff, And.intro, Set.uIcc
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
hlt : c < max a b
⊢ [[a, b]] \ {c} ∈ 𝓝[Ici c \ {c}] c

Tactic:
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsGE_of_mem ⟨hc.1, hlt⟩) _

Premises used: Icc_mem_nhdsGE_of_mem, And.left, diff_mem_nhdsWithin_diff, And.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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
obtain :
  ∀ (l : Filter ℝ) (hl : TendstoIxxClass Icc l l) (hl' : l.NeBot) (hle : l ≤ 𝓝 c) (hmem : [[a, b]] \ {c} ∈ l),
    ¬IntervalIntegrable g volume a b
⊢ ¬IntervalIntegrable g volume a b

Tactic:
obtain ⟨l, hl, hl', hle, hmem⟩ :
    ∃ l : Filter ℝ, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ {c} ∈ l := by
    rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt
    · refine ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩
      rw [← Iic_diff_right]
      exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsLE_of_mem ⟨hlt, hc.2⟩) _
    · refine ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, ?_⟩
      rw [← Ici_diff_left]
      exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsGE_of_mem ⟨hc.1, hlt⟩) _

Premises used: Real, nhds, Filter
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : l.NeBot
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
⊢ l ≤ 𝓝[[[a, b]] \ {c}] c

Tactic:
have : l ≤ 𝓝[[[a, b]] \ {c}] c := le_inf hle (le_principal_iff.2 hmem)
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : l.NeBot
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
this : l ≤ 𝓝[[[a, b]] \ {c}] c
⊢ ¬IntervalIntegrable g volume a b

Tactic:
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter l
    (mem_of_superset hmem diff_subset) (h_deriv.filter_mono this) (h_infty.mono_left this)
    (hg.mono this)

Premises used: Set.diff_subset, Filter.Eventually.filter_mono, not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter, Asymptotics.IsBigO.mono, Filter.Tendsto.mono_left, Filter.mem_of_superset
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
hne : a ≠ b
hc : c ∈ [[a, b]]
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[[[a, b]] \ {c}] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[[[a, b]] \ {c}] c) atTop
hg : deriv f =O[𝓝[[[a, b]] \ {c}] c] g
l : Filter ℝ
hl : TendstoIxxClass Icc l l
hl' : l.NeBot
hle : l ≤ 𝓝 c
hmem : [[a, b]] \ {c} ∈ l
this : l ≤ 𝓝[[[a, b]] \ {c}] c
⊢ ¬IntervalIntegrable g volume a b

Tactic:
exact not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter l
    (mem_of_superset hmem diff_subset) (h_deriv.filter_mono this) (h_infty.mono_left this)
    (hg.mono this)

Premises used: Set.diff_subset, Filter.Eventually.filter_mono, not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter, Asymptotics.IsBigO.mono, Filter.Tendsto.mono_left, Filter.mem_of_superset
-- 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
f : ℝ → E
g : ℝ → F
a b c : ℝ
h_deriv : ∀ᶠ (x : ℝ) in 𝓝[≠] c, DifferentiableAt ℝ f x
h_infty : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x‖) (𝓝[≠] c) atTop
hg : deriv f =O[𝓝[≠] c] g
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ¬IntervalIntegrable g volume a b

Tactic:
have : 𝓝[[[a, b]] \ {c}] c ≤ 𝓝[≠] c := nhdsWithin_mono _ inter_subset_right
  not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton hne hc
    (h_deriv.filter_mono this) (h_infty.mono_left this) (hg.mono this)

Premises used: Filter.Eventually.filter_mono, not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton, Asymptotics.IsBigO.mono, Filter.Tendsto.mono_left, nhdsWithin_mono, Set.inter_subset_right
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {c}ᶜ x), HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : Membership.mem (γ := Set ℝ) {c}ᶜ x
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x

Tactic:
simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)

Premises used: Iff.mpr, sub_ne_zero, HasDerivAt.log, HasDerivAt.sub_const, hasDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x

Tactic:
have A : ∀ᶠ x in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop

Tactic:
tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)

Premises used: Filter.tendsto_abs_atBot_atTop, Filter.Tendsto.comp, Real.tendsto_log_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop

Tactic:
refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)

Premises used: Filter.tendsto_abs_atBot_atTop, Filter.Tendsto.comp, Real.tendsto_log_nhdsNE_zero
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
rw : Tendsto (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] (c - c))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] 0)

Tactic:
rw [← sub_self c]

Premises used: sub_self
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] (c - c))

Tactic:
((hasDerivAt_id c).sub_const c).tendsto_nhdsNE one_ne_zero

Premises used: Set.Mem, setOf, HasDerivAt.tendsto_nhdsNE, HasDerivAt.sub_const, hasDerivAt_id, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun (x : ℝ) ↦ x - c) (𝓝[≠] c) (𝓝[≠] (c - c))

Tactic:
exact ((hasDerivAt_id c).sub_const c).tendsto_nhdsNE one_ne_zero

Premises used: HasDerivAt.tendsto_nhdsNE, HasDerivAt.sub_const, hasDerivAt_id, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop

Tactic:
have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop := by
    refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)
    rw [← sub_self c]
    exact ((hasDerivAt_id c).sub_const c).tendsto_nhdsNE one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
B : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop
⊢ ¬IntervalIntegrable f volume a b

Tactic:
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured
    (A.mono fun x hx => hx.differentiableAt) B
    (hf.congr' (A.mono fun x hx => hx.deriv.symm) EventuallyEq.rfl) hne hc

Premises used: HasDerivAt.differentiableAt, HasDerivAt.deriv, Filter.Eventually.mono, Asymptotics.IsBigO.congr', not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured, Filter.EventuallyEq.rfl, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
F : Type u_2
inst : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : IsBigO (E := ℝ) (𝓝[≠] c) (fun (x : ℝ) ↦ (x - c)⁻¹) f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun (x : ℝ) ↦ Real.log (x - c)) (x - c)⁻¹ x
B : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop
⊢ ¬IntervalIntegrable f volume a b

Tactic:
exact not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured
    (A.mono fun x hx => hx.differentiableAt) B
    (hf.congr' (A.mono fun x hx => hx.deriv.symm) EventuallyEq.rfl) hne hc

Premises used: HasDerivAt.differentiableAt, HasDerivAt.deriv, Filter.Eventually.mono, Asymptotics.IsBigO.congr', not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured, Filter.EventuallyEq.rfl, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
mp : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]
mpr : a = b ∨ c ∉ [[a, b]] → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [[a, b]]

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]

Tactic:
fun h => or_iff_not_imp_left.2 fun hne hc => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
mp : ∀ (h : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b) (hne : ¬a = b) (hc : c ∈ [[a, b]]), False
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b → a = b ∨ c ∉ [[a, b]]

Tactic:
refine fun h => or_iff_not_imp_left.2 fun hne hc => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
h : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b
hne : ¬a = b
hc : c ∈ [[a, b]]
⊢ False

Tactic:
not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h

Premises used: not_intervalIntegrable_of_sub_inv_isBigO_punctured, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
h : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b
hne : ¬a = b
hc : c ∈ [[a, b]]
⊢ False

Tactic:
exact not_intervalIntegrable_of_sub_inv_isBigO_punctured (isBigO_refl _ _) hne hc h

Premises used: not_intervalIntegrable_of_sub_inv_isBigO_punctured, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a c : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a a

Tactic:
IntervalIntegrable.refl

Premises used: IntervalIntegrable.refl
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a c : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a a

Tactic:
exact IntervalIntegrable.refl

Premises used: IntervalIntegrable.refl
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b

Tactic:
((continuous_sub_right c).continuousOn.inv₀ ?_).intervalIntegrable

Premises used: Continuous.continuousOn, ContinuousOn.inv₀, ContinuousOn.intervalIntegrable, continuous_sub_right
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
h₀ : c ∉ [[a, b]]
mpr : ∀ x ∈ [[a, b]], x - c ≠ 0
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - c)⁻¹) volume a b

Tactic:
refine ((continuous_sub_right c).continuousOn.inv₀ ?_).intervalIntegrable

Premises used: Continuous.continuousOn, ContinuousOn.inv₀, ContinuousOn.intervalIntegrable, continuous_sub_right
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ ∀ x ∈ [[a, b]], x - c ≠ 0

Tactic:
fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀

Premises used: Iff.mpr, sub_ne_zero, ne_of_mem_of_not_mem
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b c : ℝ
h₀ : c ∉ [[a, b]]
⊢ ∀ x ∈ [[a, b]], x - c ≠ 0

Tactic:
exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀

Premises used: Iff.mpr, sub_ne_zero, ne_of_mem_of_not_mem
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a b : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x⁻¹) volume a b ↔ a = b ∨ 0 ∉ [[a, b]]

Tactic:
simp only [← intervalIntegrable_sub_inv_iff, sub_zero]

Premises used: sub_zero, intervalIntegrable_sub_inv_iff
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x

Tactic:
Real.hasDerivAt_log (ne_of_gt hx)

Premises used: ne_of_gt, Real.hasDerivAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a : ℝ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ioi 0) x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x), HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x

Tactic:
filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable
Goal:
a : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun (x : ℝ) ↦ Real.log x) x⁻¹ x

Tactic:
have A : ∀ᶠ x in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x := by
    filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)