awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : (↑x : ℂ) ≠ 0
inr : cexp (log (↑x : ℂ) * y) = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
inr₁ : cexp (log (↑x : ℂ) * y) = cexp (log (-(↑x : ℂ)) * y) * cexp ((↑π : ℂ) * I * y)
inr₂ : cexp (log (↑x : ℂ) * y) = cexp (log (-(↑x : ℂ)) * y + (↑π : ℂ) * I * y)
inr₃ : cexp (log (↑x : ℂ) * y) = cexp ((log (-(↑x : ℂ)) + (↑π : ℂ) * I) * y)
inr₄ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑x : ℂ).arg : ℂ) * I) * y) = cexp ((log (-(↑x : ℂ)) + (↑π : ℂ) * I) * y)
inr₅ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑x : ℂ).arg : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖-(↑x : ℂ)‖) : ℂ) + (↑(-(↑x : ℂ)).arg : ℂ) * I + (↑π : ℂ) * I) * y)
inr₆ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑x : ℂ).arg : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(-(↑x : ℂ)).arg : ℂ) * I + (↑π : ℂ) * I) * y)
inr₇ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(-(↑x : ℂ)).arg : ℂ) * I + (↑π : ℂ) * I) * y)
inr₈ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑(-x) : ℂ).arg : ℂ) * I + (↑π : ℂ) * I) * y)
inr₉ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑0 : ℂ) * I + (↑π : ℂ) * I) * y)
inr₁₀ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + 0 * I + (↑π : ℂ) * I) * y)
inr₁₁ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
    cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + 0 + (↑π : ℂ) * I) * y)
inr₁₂ inr₁₃ :
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) = cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)

Tactic:
rw [cpow_def_of_ne_zero hne, cpow_def_of_ne_zero (neg_ne_zero.2 hne), ← exp_add, ← add_mul, log,
    log, norm_neg, arg_ofReal_of_neg hlt, ← ofReal_neg, arg_ofReal_of_nonneg (neg_nonneg.2 hx),
    ofReal_zero, zero_mul, add_zero]

Premises used: Iff.mpr, add_mul, Complex.log, Complex.exp_add, MulZeroClass.zero_mul, Complex.arg_ofReal_of_nonneg, Complex.ofReal_neg, neg_nonneg, Complex.ofReal_zero, norm_neg, neg_ne_zero, Complex.arg_ofReal_of_neg, add_zero, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
inl :
  HPow.hPow (α := ℂ) 0 (↑y : ℂ) =
    (↑(Norm.norm (E := ℂ) 0 ^ y) : ℂ) * ((↑(Real.cos (arg 0 * y)) : ℂ) + (↑(Real.sin (arg 0 * y)) : ℂ) * I)
inr :
  ∀ (hx : x ≠ 0), x ^ (↑y : ℂ) = (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)
⊢ x ^ (↑y : ℂ) = (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
y : ℝ
⊢ HPow.hPow (α := ℂ) 0 (↑y : ℂ) =
    (↑(Norm.norm (E := ℂ) 0 ^ y) : ℂ) * ((↑(Real.cos (arg 0 * y)) : ℂ) + (↑(Real.sin (arg 0 * y)) : ℂ) * I)

Tactic:
simp [ofReal_cpow le_rfl]

Premises used: le_rfl, Complex.ofReal_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
inr :
  cexp (↑((↑y : ℂ) * log x).re : ℂ) * (cos (↑((↑y : ℂ) * log x).im : ℂ) + sin (↑((↑y : ℂ) * log x).im : ℂ) * I) =
    (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)
⊢ x ^ (↑y : ℂ) = (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)

Tactic:
rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]

Premises used: Complex.log, mul_comm, Complex.exp_eq_exp_re_mul_sin_add_cos, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
inr :
  (↑(rexp ((↑y : ℂ) * log x).re) : ℂ) *
      ((↑(Real.cos ((↑y : ℂ) * log x).im) : ℂ) + (↑(Real.sin ((↑y : ℂ) * log x).im) : ℂ) * I) =
    (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)
⊢ cexp (↑((↑y : ℂ) * log x).re : ℂ) * (cos (↑((↑y : ℂ) * log x).im : ℂ) + sin (↑((↑y : ℂ) * log x).im : ℂ) * I) =
    (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
inr : 0 < ‖x‖
⊢ (↑(rexp ((↑y : ℂ) * log x).re) : ℂ) *
      ((↑(Real.cos ((↑y : ℂ) * log x).im) : ℂ) + (↑(Real.sin ((↑y : ℂ) * log x).im) : ℂ) * I) =
    (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)

Tactic:
rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul,
      Real.exp_log]

Premises used: Complex.log_re, Real.exp_mul, Real.exp_log, Complex.log_im, mul_comm, Complex.im_ofReal_mul, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
inr inr₁ inr₂ inr₃ : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
rwa [norm_pos_iff]

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
rw :
  ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).re =
    ‖x‖ ^ y * Real.cos (x.arg * y)
⊢ (x ^ (↑y : ℂ)).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
rw [cpow_ofReal]

Premises used: Complex.cpow_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
generalize : ∀ (z : ℝ), ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos z) : ℂ) + (↑(Real.sin z) : ℂ) * I)).re = ‖x‖ ^ y * Real.cos z
⊢ ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).re =
    ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
generalize arg x * y = z

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y z : ℝ
⊢ ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos z) : ℂ) + (↑(Real.sin z) : ℂ) * I)).re = ‖x‖ ^ y * Real.cos z

Tactic:
simp [Real.cos]

Premises used: Real.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
rw :
  ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).im =
    ‖x‖ ^ y * Real.sin (x.arg * y)
⊢ (x ^ (↑y : ℂ)).im = ‖x‖ ^ y * Real.sin (x.arg * y)

Tactic:
rw [cpow_ofReal]

Premises used: Complex.cpow_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
generalize : ∀ (z : ℝ), ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos z) : ℂ) + (↑(Real.sin z) : ℂ) * I)).im = ‖x‖ ^ y * Real.sin z
⊢ ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).im =
    ‖x‖ ^ y * Real.sin (x.arg * y)

Tactic:
generalize arg x * y = z

Premises used: Complex.arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y z : ℝ
⊢ ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos z) : ℂ) + (↑(Real.sin z) : ℂ) * I)).im = ‖x‖ ^ y * Real.sin z

Tactic:
simp [Real.sin]

Premises used: Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z : ℂ
hz : z ≠ 0
w : ℂ
rw : ‖cexp (log z * w)‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
rw₁ : rexp (log z * w).re = ‖z‖ ^ w.re / rexp (z.arg * w.im)
rw₂ : rexp ((log z).re * w.re - (log z).im * w.im) = ‖z‖ ^ w.re / rexp (z.arg * w.im)
rw₃ : rexp (Real.log ‖z‖ * w.re - (log z).im * w.im) = ‖z‖ ^ w.re / rexp (z.arg * w.im)
rw₄ : rexp (Real.log ‖z‖ * w.re - z.arg * w.im) = ‖z‖ ^ w.re / rexp (z.arg * w.im)
rw₅ : rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im) = ‖z‖ ^ w.re / rexp (z.arg * w.im)
rw₆ rw₇ : rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im) = rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rw [cpow_def_of_ne_zero hz, norm_exp, mul_re, log_re, log_im, Real.exp_sub,
    Real.rpow_def_of_pos (norm_pos_iff.mpr hz)]

Premises used: Iff.mpr, Complex.log_re, norm_pos_iff, Complex.mul_re, Real.rpow_def_of_pos, Complex.log_im, Complex.norm_exp, Real.exp_sub, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
inl : ∀ (hz : z ≠ 0), ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
inr :
  ∀ (h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0),
    ‖HPow.hPow (α := ℂ) 0 w‖ = Norm.norm (E := ℂ) 0 ^ w.re / rexp (arg 0 * w.im)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rcases ne_or_eq z 0 with (hz | rfl)

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
hz : z ≠ 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
norm_cpow_of_ne_zero hz w

Premises used: Complex.norm_cpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
hz : z ≠ 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
exact norm_cpow_of_ne_zero hz w

Premises used: Complex.norm_cpow_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
inr : ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = Norm.norm (E := ℂ) 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
rw [norm_zero]

Premises used: norm_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
inr :
  ∀ (h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0), ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rcases ne_or_eq z 0 with (hz | rfl) <;> [exact norm_cpow_of_ne_zero hz w; rw [norm_zero]]

Premises used: ne_or_eq, norm_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
inr : ∀ (hw : w.re = 0), ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
inr₁ : ∀ (hw : w.re ≠ 0), ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)

Tactic:
rcases eq_or_ne w.re 0 with hw | hw

Premises used: Complex.re, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)

Tactic:
simp [h rfl hw]

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
inr : w ≠ 0
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)

Tactic:
rw [Real.zero_rpow hw, zero_div, zero_cpow, norm_zero]

Premises used: norm_zero, zero_div, Real.zero_rpow, Complex.zero_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0

Tactic:
ne_of_apply_ne re hw

Premises used: ne_of_apply_ne, Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0

Tactic:
exact ne_of_apply_ne re hw

Premises used: ne_of_apply_ne, Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
pos : ∀ (h : z = 0 → w.re = 0 → w = 0), ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
neg : ∀ (h : z = 0 ∧ w.re = 0 ∧ w ≠ 0), ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by_cases! h : z = 0 → w.re = 0 → w = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
(norm_cpow_of_imp h).le

Premises used: Complex.norm_cpow_of_imp, Eq.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
exact (norm_cpow_of_imp h).le

Premises used: Complex.norm_cpow_of_imp, Eq.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
rw : ‖x‖ ^ (↑y : ℂ).re / rexp (x.arg * (↑y : ℂ).im) = ‖x‖ ^ y
rw₁ : x = 0 → (↑y : ℂ).re = 0 → (↑y : ℂ) = 0
⊢ ‖x ^ (↑y : ℂ)‖ = ‖x‖ ^ y

Tactic:
rw [norm_cpow_of_imp]

Premises used: Complex.norm_cpow_of_imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
⊢ ‖x‖ ^ (↑y : ℂ).re / rexp (x.arg * (↑y : ℂ).im) = ‖x‖ ^ y

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
y : ℝ
⊢ x = 0 → (↑y : ℂ).re = 0 → (↑y : ℂ) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
n : ℕ
rw : ‖HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹‖ = ‖x ^ (↑(↑n : ℝ)⁻¹ : ℂ)‖
⊢ ‖HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹‖ = HPow.hPow (β := ℝ) ‖x‖ (↑n : ℝ)⁻¹

Tactic:
rw [← norm_cpow_real]

Premises used: Complex.norm_cpow_real
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℂ
n : ℕ
⊢ ‖HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹‖ = ‖x ^ (↑(↑n : ℝ)⁻¹ : ℂ)‖

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 < x
y : ℂ
rw : ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = x ^ y.re
rw₁ : ‖(↑x : ℂ)‖ ^ y.re / rexp (0 * y.im) = x ^ y.re
rw₂ : ‖(↑x : ℂ)‖ ^ y.re / rexp 0 = x ^ y.re
rw₃ : ‖(↑x : ℂ)‖ ^ y.re / 1 = x ^ y.re
rw₄ : ‖(↑x : ℂ)‖ ^ y.re = x ^ y.re
rw₅ rw₆ : x ^ y.re = x ^ y.re
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re

Tactic:
rw [norm_cpow_of_ne_zero (ofReal_ne_zero.mpr hx.ne'), arg_ofReal_of_nonneg hx.le,
    zero_mul, Real.exp_zero, div_one, Complex.norm_of_nonneg hx.le]

Premises used: Iff.mpr, MulZeroClass.zero_mul, Complex.arg_ofReal_of_nonneg, Complex.norm_cpow_of_ne_zero, Complex.ofReal_ne_zero, LT.lt.le, Complex.norm_of_nonneg, LT.lt.ne', Real.exp_zero, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
rw : ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = x ^ y.re
rw₁ : (↑x : ℂ) = 0 → y.re = 0 → y = 0
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re

Tactic:
rw [norm_cpow_of_imp]

Premises used: Complex.norm_cpow_of_imp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = x ^ y.re

Tactic:
simp [*, arg_ofReal_of_nonneg, abs_of_nonneg]

Premises used: Complex.arg_ofReal_of_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ (↑x : ℂ) = 0 → y.re = 0 → y = 0

Tactic:
simp [*, arg_ofReal_of_nonneg, abs_of_nonneg]

Premises used: Complex.arg_ofReal_of_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
c : ℂ
h : ∀ (t : ℝ) (ht : 0 < t), ‖(↑t : ℂ) ^ c‖ = t ^ c.re
⊢ EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ c‖) fun (t : ℝ) ↦ t ^ c.re

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
c : ℂ
t : ℝ
ht : 0 < t
h h₁ : t ^ c.re = t ^ c.re
⊢ ‖(↑t : ℂ) ^ c‖ = t ^ c.re

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos ht]

Premises used: Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
s : ℂ
hs : s.re ≠ 0
rw : ‖(↑(↑n : ℝ) : ℂ) ^ s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
rw₁ rw₂ : HPow.hPow (α := ℝ) (↑n : ℝ) s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs]

Premises used: Nat.cast_nonneg, Complex.ofReal_natCast, Complex.norm_cpow_eq_rpow_re_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : 0 < n
s : ℂ
rw : ‖(↑(↑n : ℝ) : ℂ) ^ s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
rw₁ rw₂ : HPow.hPow (α := ℝ) (↑n : ℝ) s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re

Tactic:
rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr hn) _]

Premises used: Iff.mpr, Nat.cast_pos, Complex.ofReal_natCast, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
n : ℕ
hn : 0 < n
s : ℂ
⊢ 0 < ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖

Tactic:
(norm_natCast_cpow_of_pos hn _).symm ▸ Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _

Premises used: Iff.mpr, Real.rpow_pos_of_pos, Nat.cast_pos, Eq.rec, Complex.norm_natCast_cpow_of_pos, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
h₁ : -π < (log (↑x : ℂ) * (↑y : ℂ)).im
h₂ : (log (↑x : ℂ) * (↑y : ℂ)).im ≤ π
⊢ (↑x : ℂ) ^ ((↑y : ℂ) * z) = (↑(x ^ y) : ℂ) ^ z

Tactic:
rw [cpow_mul, ofReal_cpow hx]

Premises used: Complex.ofReal_cpow, Complex.cpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
h₁ : 0 < π
⊢ -π < (log (↑x : ℂ) * (↑y : ℂ)).im

Tactic:
rw [← ofReal_log hx, ← ofReal_mul, ofReal_im, neg_lt_zero]

Premises used: Complex.ofReal_log, neg_lt_zero, Complex.ofReal_im, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π

Tactic:
Real.pi_pos

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π

Tactic:
exact Real.pi_pos

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
h₂ : 0 ≤ π
⊢ (log (↑x : ℂ) * (↑y : ℂ)).im ≤ π

Tactic:
rw [← ofReal_log hx, ← ofReal_mul, ofReal_im]

Premises used: Complex.ofReal_log, Complex.ofReal_im, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 ≤ π

Tactic:
Real.pi_pos.le

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 ≤ π

Tactic:
exact Real.pi_pos.le

Premises used: Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h₁ : -π < (Complex.log (↑x : ℂ) * (↑y : ℂ)).im
h₂ : (Complex.log (↑x : ℂ) * (↑y : ℂ)).im ≤ π
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg hx _),
      Complex.ofReal_cpow hx, Complex.ofReal_mul, Complex.cpow_mul, Complex.ofReal_cpow hx]

Premises used: Complex.ofReal_cpow, Complex.cpow_mul, Complex.ofReal_inj, Real.rpow_nonneg, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log (↑x : ℂ) * (↑y : ℂ)).im

Tactic:
simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im,
      neg_lt_zero, pi_pos, le_of_lt pi_pos]

Premises used: Complex.ofReal_log, le_of_lt, Real.pi_pos, neg_lt_zero, Complex.ofReal_im, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log (↑x : ℂ) * (↑y : ℂ)).im ≤ π

Tactic:
simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im,
      neg_lt_zero, pi_pos, le_of_lt pi_pos]

Premises used: Complex.ofReal_log, le_of_lt, Real.pi_pos, neg_lt_zero, Complex.ofReal_im, Eq.symm, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
simp_rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = HPow.hPow (β := ℝ) x (↑n : ℝ) ^ y
simp_rw₁ : x ^ (y * (↑n : ℝ)) = x ^ ((↑n : ℝ) * y)
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
simp_rw [← rpow_natCast, ← rpow_mul hx, mul_comm y]

Premises used: mul_comm, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
simp_rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = HPow.hPow (β := ℝ) x (↑n : ℝ) ^ y
simp_rw₁ : x ^ (y * (↑n : ℝ)) = x ^ ((↑n : ℝ) * y)
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
simp_rw [← rpow_intCast, ← rpow_mul hx, mul_comm y]

Premises used: mul_comm, Real.rpow_mul, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
rw : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = x ^ y * x ^ n
rw₁ : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₂ : ((↑x : ℂ) ^ ((↑y : ℂ) + (↑(↑n : ℝ) : ℂ))).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₃ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑x : ℂ) ^ (↑(↑n : ℝ) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₄ : ((↑x : ℂ) ^ (↑y : ℂ) * HPow.hPow (β := ℂ) (↑x : ℂ) (↑n : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₅ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑x : ℂ) ^ n).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₆ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑(x ^ n) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₇ : ((↑(x ^ n) : ℂ) * (↑x : ℂ) ^ (↑y : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₈ : x ^ n * ((↑x : ℂ) ^ (↑y : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
rw₉ rw₁₀ : ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n = ((↑x : ℂ) ^ (↑y : ℂ)).re * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
rw [rpow_def, rpow_def, Complex.ofReal_add,
    Complex.cpow_add _ _ (Complex.ofReal_ne_zero.mpr hx), Complex.ofReal_intCast,
    Complex.cpow_intCast, ← Complex.ofReal_zpow, mul_comm, Complex.re_ofReal_mul, mul_comm]

Premises used: Complex.cpow_intCast, Iff.mpr, Complex.ofReal_zpow, Complex.ofReal_ne_zero, Complex.ofReal_intCast, Complex.ofReal_add, Complex.cpow_add, mul_comm, Real.rpow_def, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
simpa using rpow_add_intCast hx y n

Premises used: Nat.cast, Real.rpow_add_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
simpa using rpow_add_intCast hx y (-n)

Premises used: Real.rpow_add_intCast, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
simpa using rpow_sub_intCast hx y n

Premises used: Nat.cast, Real.rpow_sub_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + (↑n : ℝ) ≠ 0
rw : x ^ y * HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y * x ^ n
rw₁ rw₂ : x ^ y * x ^ n = x ^ y * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
rw [rpow_add' hx h, rpow_intCast]

Premises used: Real.rpow_add', Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + (↑n : ℝ) ≠ 0
rw : x ^ y * HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y * x ^ n
rw₁ rw₂ : x ^ y * x ^ n = x ^ y * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n

Tactic:
rw [rpow_add' hx h, rpow_natCast]

Premises used: Real.rpow_add', Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - (↑n : ℝ) ≠ 0
rw : x ^ y / HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y / x ^ n
rw₁ rw₂ : x ^ y / x ^ n = x ^ y / x ^ n
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
rw [rpow_sub' hx h, rpow_intCast]

Premises used: Real.rpow_sub', Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - (↑n : ℝ) ≠ 0
rw : x ^ y / HPow.hPow (β := ℝ) x (↑n : ℝ) = x ^ y / x ^ n
rw₁ rw₂ : x ^ y / x ^ n = x ^ y / x ^ n
⊢ x ^ (y - (↑n : ℝ)) = x ^ y / x ^ n

Tactic:
rw [rpow_sub' hx h, rpow_natCast]

Premises used: Real.rpow_sub', Real.rpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using rpow_add_natCast hx y 1

Premises used: Real.rpow_add_natCast, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
simpa using rpow_sub_natCast hx y 1

Premises used: Real.rpow_sub_natCast, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
rw : x ^ y * HPow.hPow (β := ℝ) x 1 = x ^ y * x
rw₁ rw₂ : x ^ y * x = x ^ y * x
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
rw [rpow_add' hx h, rpow_one]

Premises used: Real.rpow_one, Real.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
rw : HPow.hPow (β := ℝ) x 1 * x ^ y = x * x ^ y
rw₁ rw₂ : x * x ^ y = x * x ^ y
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
rw [rpow_add' hx h, rpow_one]

Premises used: Real.rpow_one, Real.rpow_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Real
Goal:
x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
rw : x ^ y / HPow.hPow (β := ℝ) x 1 = x ^ y / x
rw₁ rw₂ : x ^ y / x = x ^ y / x
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
rw [rpow_sub' hx h, rpow_one]

Premises used: Real.rpow_sub', Real.rpow_one