-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
@[fun_prop]
lemma continuous_mul_log : Continuous fun x ↦ x * log x

Proof state:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)

Tactic:
simp only [nhdsWithin_singleton, sup_le_iff, Filter.nonpos_iff, Filter.tendsto_sup]

Result:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ (Filter.Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0) ∧ Filter.Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)) ∧
    Filter.Tendsto (fun x => log x * x) (pure 0) (𝓝 0)

Proof state:
⊢ Continuous fun x => x * log x

Tactic:
rw [continuous_iff_continuousAt]

Result:
⊢ ∀ (x : ℝ), ContinuousAt (fun x => x * log x) x

Proof state:
case inr

⊢ Filter.Tendsto (fun x => log x * x) (𝓝 0) (𝓝 0)

Tactic:
nth_rewrite 1 [← nhdsWithin_univ]

Result:
case inr

⊢ Filter.Tendsto (fun x => log x * x) (𝓝[Set.univ] 0) (𝓝 0)

Proof state:
x : ℝ
⊢ ContinuousAt (fun x => x * log x) x

Tactic:
obtain hx | rfl := ne_or_eq x 0

Result:
case inl
x : ℝ
hx : x ≠ 0
⊢ ContinuousAt (fun x => x * log x) x

case inr

⊢ ContinuousAt (fun x => x * log x) 0

Proof state:
case inr

⊢ Filter.Tendsto (fun x => x * log x) (𝓝 0) (𝓝 0)

Tactic:
simp_rw [mul_comm _ (log _)]

Result:
case inr

⊢ Filter.Tendsto (fun x => log x * x) (𝓝 0) (𝓝 0)

Proof state:
case inr.refine_2
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (pure 0) (𝓝 0)

Tactic:
convert tendsto_pure_nhds (fun x ↦ log x * x) 0

Result:
case h.e'_5.h.e'_3
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ 0 = log 0 * 0

Proof state:
case inr.refine_1
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)

Tactic:
simpa only [rpow_one] using tendsto_log_mul_rpow_nhds_zero zero_lt_one

Result:
no goals

Proof state:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (𝓝[Set.univ] 0) (𝓝 0)

Tactic:
rw [this, nhdsWithin_union, nhdsWithin_union]

Result:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (𝓝[<] 0 ⊔ 𝓝[>] 0 ⊔ 𝓝[{0}] 0) (𝓝 0)

Proof state:
case inr

⊢ Filter.Tendsto (fun x => log x * x) (𝓝[Set.univ] 0) (𝓝 0)

Tactic:
have : (Set.univ : Set ℝ) = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0} := by ext; simp [em]

Result:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (𝓝[Set.univ] 0) (𝓝 0)

Proof state:
case inr
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ (Filter.Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0) ∧ Filter.Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)) ∧
    Filter.Tendsto (fun x => log x * x) (pure 0) (𝓝 0)

Tactic:
refine ⟨⟨tendsto_log_mul_self_nhds_zero_left, ?_⟩, ?_⟩

Result:
case inr.refine_1
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)

case inr.refine_2
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x => log x * x) (pure 0) (𝓝 0)

Proof state:
case h
x✝ : ℝ
⊢ x✝ ∈ Set.univ ↔ x✝ ∈ Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}

Tactic:
simp [em]

Result:
no goals

Proof state:
⊢ Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ x✝ ∈ Set.univ ↔ x✝ ∈ Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}

Proof state:
case inl
x : ℝ
hx : x ≠ 0
⊢ ContinuousAt (fun x => x * log x) x

Tactic:
exact (continuous_id'.continuousAt).mul (continuousAt_log hx)

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ 0 = log 0 * 0

Tactic:
simp

Result:
no goals

Proof state:
case inr

⊢ ContinuousAt (fun x => x * log x) 0

Tactic:
rw [ContinuousAt, zero_mul]

Result:
case inr

⊢ Filter.Tendsto (fun x => x * log x) (𝓝 0) (𝓝 0)

Proof state:
⊢ ∀ (x : ℝ), ContinuousAt (fun x => x * log x) x

Tactic:
intro x

Result:
x : ℝ
⊢ ContinuousAt (fun x => x * log x) x