-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_intervalIntegrable_of_sub_inv_isBigO_punctured {f : ℝ → F} {a b c : ℝ}
    (hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f) (hne : a ≠ b) (hc : c ∈ [[a, b]]) :
    ¬IntervalIntegrable f volume a b

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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

Result:
no goals

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Result:
case h
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : x ∈ {c}ᶜ
⊢ HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x

Proof state:
case h
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
x : ℝ
hx : x ∈ {c}ᶜ
⊢ 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)

Result:
no goals

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ¬IntervalIntegrable f volume a b

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)

Result:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ ¬IntervalIntegrable f volume a b

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x
⊢ ¬IntervalIntegrable f volume a b

Tactic:
have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop := by
  refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp ?_)
  rw [← sub_self c]
  exact ((hasDerivAt_id c).sub_const c).tendsto_punctured_nhds one_ne_zero

Result:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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_punctured_nhds one_ne_zero

Result:
no goals

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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) (𝓝[≠] 0)

Tactic:
rw [← sub_self c]

Result:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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))

Proof state:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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:
refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsWithin_zero.comp ?_)

Result:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] 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) (𝓝[≠] 0)