-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
lemma tendsto_log_mul_self_nhds_zero_left : Filter.Tendsto (fun x ↦ log x * x) (𝓝[<] 0) (𝓝 0)

Proof state:
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
have h := tendsto_log_mul_rpow_nhds_zero zero_lt_one

Result:
h : Tendsto (fun x => log x * x ^ 1) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
x : ℝ
hx : x < 0
⊢ x ∈ {0}ᶜ

Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, hx.ne, not_false_eq_true]

Result:
no goals

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ Tendsto (-(fun x => log x * x) ∘ fun x => |x|) (𝓝[<] 0) (𝓝 0)

Tactic:
nth_rewrite 3 [← neg_zero]

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ Tendsto (-(fun x => log x * x) ∘ fun x => |x|) (𝓝[<] 0) (𝓝 (-0))

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x

Tactic:
simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ x < 0, -(log x * |x|) = log x * x

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ 𝓝[<] 0 ≤ 𝓝[≠] 0

Tactic:
refine nhdsWithin_mono 0 (fun x hx ↦ ?_)

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
x : ℝ
hx : x ∈ Set.Iio 0
⊢ x ∈ {0}ᶜ

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
x : ℝ
hx : x < 0
⊢ -(log x * |x|) = log x * x

Tactic:
simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]

Result:
no goals

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
⊢ ∀ x < 0, -(log x * |x|) = log x * x

Tactic:
intro x hx

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
x : ℝ
hx : x < 0
⊢ -(log x * |x|) = log x * x

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
refine tendsto_nhdsWithin_congr h_eq ?_

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ Tendsto (-(fun x => log x * x) ∘ fun x => |x|) (𝓝[<] 0) (𝓝 0)

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
have h_eq : ∀ x ∈ Set.Iio 0, (- (fun x ↦ log x * x) ∘ (fun x ↦ |x|)) x = log x * x := by
  simp only [Set.mem_Iio, Pi.neg_apply, Function.comp_apply, log_abs]
  intro x hx
  simp only [abs_of_nonpos hx.le, mul_neg, neg_neg]

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ Tendsto (-(fun x => log x * x) ∘ fun x => |x|) (𝓝[<] 0) (𝓝 (-0))

Tactic:
refine (h.comp (tendsto_abs_nhdsWithin_zero.mono_left ?_)).neg

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
⊢ 𝓝[<] 0 ≤ 𝓝[≠] 0

Proof state:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
x : ℝ
hx : x ∈ Set.Iio 0
⊢ x ∈ {0}ᶜ

Tactic:
simp only [Set.mem_Iio] at hx

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x
x : ℝ
hx : x < 0
⊢ x ∈ {0}ᶜ

Proof state:
h : Tendsto (fun x => log x * x ^ 1) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)

Tactic:
simp only [Real.rpow_one] at h

Result:
h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)