-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : 0 < p.1
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
h :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    rexp (log p.1 * p.2) •
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
        p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))
h₁ :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    p.1 ^ p.2 •
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
        p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))
h₂ :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    p.1 ^ p.2 • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      p.1 ^ p.2 • p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ)
h₃ :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      p.1 ^ p.2 • p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ)
h₄ :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * (p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      p.1 ^ p.2 • p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ)
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    rexp (log p.1 * p.2) •
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
        p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))
have h₅ : HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * (p.2 * p.1⁻¹)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
  HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
    p.1 ^ p.2 • p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ)
Tactic: rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm,
    div_eq_mul_inv, smul_smul, smul_smul, mul_assoc, add_comm]