awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
have this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
Tactic: have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
    (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
-- 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)
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
have refine : HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2))
  (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ))
  p
Tactic: refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
-- 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)
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2))
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
have h : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
    Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
      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 ℝ ℝ ℝ))
Tactic: convert! ((hasStrictFDerivAt_fst.log hp.ne').fun_mul hasStrictFDerivAt_snd).exp using 1
-- 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
⊢ 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.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 ℝ ℝ ℝ))
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]
-- 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 ℝ ℝ ℝ))
⊢ 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.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 ℝ ℝ ℝ))
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]
-- 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 ℝ ℝ ℝ))
⊢ 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.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 ℝ ℝ ℝ)
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]
-- 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 ℝ ℝ ℝ)
⊢ 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.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 ℝ ℝ ℝ)
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]
-- 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 ℝ ℝ ℝ)
⊢ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
have this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
Tactic: have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π) :=
    (continuousAt_fst.eventually (gt_mem_nhds hp)).mono fun p hp => rpow_def_of_neg hp _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
have refine : HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π))
  (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
      (ContinuousLinearMap.snd ℝ ℝ ℝ))
  p
Tactic: refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π))
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
have h : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
    Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
      instAddCommGroup = Ring.toAddCommGroup →
        HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
              HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
                (ContinuousLinearMap.snd ℝ ℝ ℝ) =
            rexp (log p.1 * p.2) • -sin (p.2 * π) • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) π (ContinuousLinearMap.snd ℝ ℝ ℝ) +
              cos (p.2 * π) •
                rexp (log p.1 * p.2) •
                  (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                    p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))
Tactic: convert!
    ((hasStrictFDerivAt_fst.log hp.ne).fun_mul hasStrictFDerivAt_snd).exp.fun_mul
      (hasStrictFDerivAt_snd.mul_const π).cos using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (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
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    rexp (log p.1 * p.2) • -sin (p.2 * π) • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) π (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      cos (p.2 * π) •
        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.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
      (ContinuousLinearMap.snd ℝ ℝ ℝ) =
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
      (ContinuousLinearMap.snd ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
Tactic: simp_rw [rpow_sub_one hp.ne, smul_add, ← add_assoc, smul_smul, ← add_smul, ← mul_assoc,
    mul_comm (cos _), ← rpow_def_of_neg hp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (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
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
have h : HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
      (ContinuousLinearMap.snd ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 * p.1⁻¹)) (ContinuousLinearMap.fst ℝ ℝ ℝ) =
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
      (ContinuousLinearMap.snd ℝ ℝ ℝ) +
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
Tactic: rw [div_eq_mul_inv, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (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
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 * p.1⁻¹)) (ContinuousLinearMap.fst ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
have h : p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
  rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (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
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 * p.1⁻¹)) (ContinuousLinearMap.fst ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
have h₁ : p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
⊢ ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have inl : ∀ (hneg : p.1 < 0), ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
Tactic: rcases hp.lt_or_gt with hneg | hpos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
inl : ∀ (hneg : p.1 < 0), ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
⊢ ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have inr : ∀ (hpos : 0 < p.1), ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
Tactic: rcases hp.lt_or_gt with hneg | hpos