awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
⊢ (x ^ (↑y : ℂ)).im = ‖x‖ ^ y * Real.sin (x.arg * y)
have rw : ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).im =
  ‖x‖ ^ y * Real.sin (x.arg * y)
Tactic: rw [cpow_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
⊢ ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).im =
    ‖x‖ ^ y * Real.sin (x.arg * y)
have generalize : ∀ (z : ℝ), ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos z) : ℂ) + (↑(Real.sin z) : ℂ) * I)).im = ‖x‖ ^ y * Real.sin z
Tactic: generalize arg x * y = z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z : ℂ
hz : z ≠ 0
w : ℂ
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw : ‖cexp (log 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z : ℂ
hz : z ≠ 0
w : ℂ
rw : ‖cexp (log z * w)‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw₁ : rexp (log z * w).re = ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw₂ : rexp ((log z).re * w.re - (log z).im * w.im) = ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw₃ : rexp (Real.log ‖z‖ * w.re - (log z).im * w.im) = ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw₄ : rexp (Real.log ‖z‖ * w.re - z.arg * w.im) = ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw₅ : rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im) = ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have rw₆ : rexp (Real.log ‖z‖ * w.re) / rexp (z.arg * w.im) = rexp (Real.log ‖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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have inl : ∀ (hz : z ≠ 0), ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
Tactic: rcases ne_or_eq z 0 with (hz | rfl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have 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)
Tactic: rcases ne_or_eq z 0 with (hz | rfl)
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = Norm.norm (E := ℂ) 0 ^ w.re / rexp (arg 0 * w.im)
have inr : ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
Tactic: rw [norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)
have inr : ∀ (h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0), ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
Tactic: rcases ne_or_eq z 0 with (hz | rfl) <;> [exact norm_cpow_of_ne_zero hz w; rw [norm_zero]]
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
w : ℂ
h : Eq (α := ℂ) 0 0 → w.re = 0 → w = 0
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
have inr : ∀ (hw : w.re = 0), ‖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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ ‖HPow.hPow (α := ℂ) 0 w‖ = HPow.hPow (α := ℝ) 0 w.re / rexp (arg 0 * w.im)
have inr₁ : ∀ (hw : w.re ≠ 0), ‖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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
have inr : w ≠ 0
Tactic: rw [Real.zero_rpow hw, zero_div, zero_cpow, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z w : ℂ
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
have pos : ∀ (h : z = 0 → w.re = 0 → w = 0), ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
Tactic: by_cases! h : z = 0 → w.re = 0 → w = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
z w : ℂ
pos : ∀ (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)
have neg : ∀ (h : z = 0 ∧ w.re = 0 ∧ w ≠ 0), ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
Tactic: by_cases! h : z = 0 → w.re = 0 → w = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
⊢ ‖x ^ (↑y : ℂ)‖ = ‖x‖ ^ y
have rw : ‖x‖ ^ (↑y : ℂ).re / rexp (x.arg * (↑y : ℂ).im) = ‖x‖ ^ y
Tactic: rw [norm_cpow_of_imp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
rw : ‖x‖ ^ (↑y : ℂ).re / rexp (x.arg * (↑y : ℂ).im) = ‖x‖ ^ y
⊢ ‖x ^ (↑y : ℂ)‖ = ‖x‖ ^ y
have rw₁ : x = 0 → (↑y : ℂ).re = 0 → (↑y : ℂ) = 0
Tactic: rw [norm_cpow_of_imp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
n : ℕ
⊢ ‖HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹‖ = HPow.hPow (β := ℝ) ‖x‖ (↑n : ℝ)⁻¹
have rw : ‖HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹‖ = ‖x ^ (↑(↑n : ℝ)⁻¹ : ℂ)‖
Tactic: rw [← norm_cpow_real]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℂ
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw : ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 < x
y : ℂ
rw : ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = x ^ y.re
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw₁ : ‖(↑x : ℂ)‖ ^ y.re / rexp (0 * y.im) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw₂ : ‖(↑x : ℂ)‖ ^ y.re / rexp 0 = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw₃ : ‖(↑x : ℂ)‖ ^ y.re / 1 = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw₄ : ‖(↑x : ℂ)‖ ^ y.re = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw₅ : x ^ y.re = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw : ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = x ^ y.re
Tactic: rw [norm_cpow_of_imp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
rw : ‖(↑x : ℂ)‖ ^ y.re / rexp ((↑x : ℂ).arg * y.im) = x ^ y.re
⊢ ‖(↑x : ℂ) ^ y‖ = x ^ y.re
have rw₁ : (↑x : ℂ) = 0 → y.re = 0 → y = 0
Tactic: rw [norm_cpow_of_imp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
c : ℂ
⊢ EventuallyEq (β := ℝ) atTop (fun (t : ℝ) ↦ ‖(↑t : ℂ) ^ c‖) fun (t : ℝ) ↦ t ^ c.re
have h : ∀ (t : ℝ) (ht : 0 < t), ‖(↑t : ℂ) ^ c‖ = t ^ c.re
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
c : ℂ
t : ℝ
ht : 0 < t
⊢ ‖(↑t : ℂ) ^ c‖ = t ^ c.re
have h : t ^ c.re = t ^ c.re
Tactic: rw [norm_cpow_eq_rpow_re_of_pos ht]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
s : ℂ
hs : s.re ≠ 0
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have rw : ‖(↑(↑n : ℝ) : ℂ) ^ s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
s : ℂ
hs : s.re ≠ 0
rw : ‖(↑(↑n : ℝ) : ℂ) ^ s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have rw₁ : HPow.hPow (α := ℝ) (↑n : ℝ) s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_nonneg n.cast_nonneg hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have rw : ‖(↑(↑n : ℝ) : ℂ) ^ s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr hn) _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℂ
rw : ‖(↑(↑n : ℝ) : ℂ) ^ s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
⊢ ‖HPow.hPow (α := ℂ) (↑n : ℂ) s‖ = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
have rw₁ : HPow.hPow (α := ℝ) (↑n : ℝ) s.re = HPow.hPow (α := ℝ) (↑n : ℝ) s.re
Tactic: rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr hn) _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (↑x : ℂ) ^ ((↑y : ℂ) * z) = (↑(x ^ y) : ℂ) ^ z
have h₁ : -π < (log (↑x : ℂ) * (↑y : ℂ)).im
Tactic: rw [cpow_mul, ofReal_cpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
h₁ : -π < (log (↑x : ℂ) * (↑y : ℂ)).im
⊢ (↑x : ℂ) ^ ((↑y : ℂ) * z) = (↑(x ^ y) : ℂ) ^ z
have h₂ : (log (↑x : ℂ) * (↑y : ℂ)).im ≤ π
Tactic: rw [cpow_mul, ofReal_cpow hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log (↑x : ℂ) * (↑y : ℂ)).im
have h₁ : 0 < π
Tactic: rw [← ofReal_log hx, ← ofReal_mul, ofReal_im, neg_lt_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ (log (↑x : ℂ) * (↑y : ℂ)).im ≤ π
have h₂ : 0 ≤ π
Tactic: rw [← ofReal_log hx, ← ofReal_mul, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z
have h₁ : -π < (Complex.log (↑x : ℂ) * (↑y : ℂ)).im
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h₁ : -π < (Complex.log (↑x : ℂ) * (↑y : ℂ)).im
⊢ x ^ (y * z) = (x ^ y) ^ z
have h₂ : (Complex.log (↑x : ℂ) * (↑y : ℂ)).im ≤ π
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ n) ^ y
have simp_rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = HPow.hPow (β := ℝ) x (↑n : ℝ) ^ y
Tactic: simp_rw [← rpow_natCast, ← rpow_mul hx, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
simp_rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = HPow.hPow (β := ℝ) x (↑n : ℝ) ^ y
⊢ (x ^ y) ^ n = (x ^ n) ^ y
have simp_rw₁ : x ^ (y * (↑n : ℝ)) = x ^ ((↑n : ℝ) * y)
Tactic: simp_rw [← rpow_natCast, ← rpow_mul hx, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
⊢ (x ^ y) ^ n = (x ^ n) ^ y
have simp_rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = HPow.hPow (β := ℝ) x (↑n : ℝ) ^ y
Tactic: simp_rw [← rpow_intCast, ← rpow_mul hx, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℤ
simp_rw : HPow.hPow (β := ℝ) (x ^ y) (↑n : ℝ) = HPow.hPow (β := ℝ) x (↑n : ℝ) ^ y
⊢ (x ^ y) ^ n = (x ^ n) ^ y
have simp_rw₁ : x ^ (y * (↑n : ℝ)) = x ^ ((↑n : ℝ) * y)
Tactic: simp_rw [← rpow_intCast, ← rpow_mul hx, mul_comm y]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℤ
rw : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = x ^ y * x ^ n
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₁ : ((↑x : ℂ) ^ (↑(y + (↑n : ℝ)) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₂ : ((↑x : ℂ) ^ ((↑y : ℂ) + (↑(↑n : ℝ) : ℂ))).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₃ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑x : ℂ) ^ (↑(↑n : ℝ) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₄ : ((↑x : ℂ) ^ (↑y : ℂ) * HPow.hPow (β := ℂ) (↑x : ℂ) (↑n : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₅ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑x : ℂ) ^ n).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₆ : ((↑x : ℂ) ^ (↑y : ℂ) * (↑(x ^ n) : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₇ : ((↑(x ^ n) : ℂ) * (↑x : ℂ) ^ (↑y : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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
⊢ x ^ (y + (↑n : ℝ)) = x ^ y * x ^ n
have rw₈ : x ^ n * ((↑x : ℂ) ^ (↑y : ℂ)).re = ((↑x : ℂ) ^ (↑y : ℂ)).re * 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]