awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → -y = 0 → y = 0 → Eq (α := ℝ) 1 1⁻¹
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
have neg : x = 0 → -y = 0 → ¬y = 0 → Eq (α := ℝ) 1 0⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → -y = 0 → y = 0 → Eq (α := ℝ) 1 1⁻¹
neg : x = 0 → -y = 0 → ¬y = 0 → Eq (α := ℝ) 1 0⁻¹
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
have pos₁ : x = 0 → ¬-y = 0 → y = 0 → Eq (α := ℝ) 0 1⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → -y = 0 → y = 0 → Eq (α := ℝ) 1 1⁻¹
neg : x = 0 → -y = 0 → ¬y = 0 → Eq (α := ℝ) 1 0⁻¹
pos₁ : x = 0 → ¬-y = 0 → y = 0 → Eq (α := ℝ) 0 1⁻¹
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
have neg₁ : x = 0 → ¬-y = 0 → ¬y = 0 → Eq (α := ℝ) 0 0⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → -y = 0 → y = 0 → Eq (α := ℝ) 1 1⁻¹
neg : x = 0 → -y = 0 → ¬y = 0 → Eq (α := ℝ) 1 0⁻¹
pos₁ : x = 0 → ¬-y = 0 → y = 0 → Eq (α := ℝ) 0 1⁻¹
neg₁ : x = 0 → ¬-y = 0 → ¬y = 0 → Eq (α := ℝ) 0 0⁻¹
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
have neg₂ : ¬x = 0 → rexp (log x * -y) = (rexp (log x * y))⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y - z ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z
have h₁ : y + -z ≠ 0
Tactic: simp only [sub_eq_add_neg] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (↑(x ^ y) : ℂ) = (↑x : ℂ) ^ (↑y : ℂ)
have simp : (↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) : ℂ) =
  if x = 0 then if y = 0 then 1 else 0 else cexp (log (↑x : ℂ) * (↑y : ℂ))
Tactic: simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) : ℂ) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log (↑x : ℂ) * (↑y : ℂ))
have pos : x = 0 → y = 0 → (↑1 : ℂ) = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → y = 0 → (↑1 : ℂ) = 1
⊢ (↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) : ℂ) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log (↑x : ℂ) * (↑y : ℂ))
have neg : x = 0 → ¬y = 0 → (↑0 : ℂ) = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : 0 ≤ x
y : ℝ
pos : x = 0 → y = 0 → (↑1 : ℂ) = 1
neg : x = 0 → ¬y = 0 → (↑0 : ℂ) = 0
⊢ (↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) : ℂ) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log (↑x : ℂ) * (↑y : ℂ))
have neg₁ : ¬x = 0 → (↑(rexp (Real.log x * y)) : ℂ) = cexp (log (↑x : ℂ) * (↑y : ℂ))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inl : ∀ (hx : LE.le (α := ℝ) 0 0), (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
Tactic: rcases hx.eq_or_lt with (rfl | hlt)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
inl : ∀ (hx : LE.le (α := ℝ) 0 0), (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr : ∀ (hlt : x < 0), (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
Tactic: rcases hx.eq_or_lt with (rfl | hlt)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y : ℂ
hx : LE.le (α := ℝ) 0 0
⊢ (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inl : HPow.hPow (β := ℂ) (↑0 : ℂ) 0 = HPow.hPow (β := ℂ) (-(↑0 : ℂ)) 0 * cexp ((↑π : ℂ) * I * 0)
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
y : ℂ
hx : LE.le (α := ℝ) 0 0
inl : HPow.hPow (β := ℂ) (↑0 : ℂ) 0 = HPow.hPow (β := ℂ) (-(↑0 : ℂ)) 0 * cexp ((↑π : ℂ) * I * 0)
⊢ (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inl₁ : ∀ (hy : y ≠ 0), (↑0 : ℂ) ^ y = (-(↑0 : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have hne : (↑x : ℂ) ≠ 0
Tactic: have hne : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr hlt.ne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : (↑x : ℂ) ≠ 0
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr : cexp (log (↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : (↑x : ℂ) ≠ 0
inr : cexp (log (↑x : ℂ) * y) = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₁ : cexp (log (↑x : ℂ) * y) = cexp (log (-(↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₂ : cexp (log (↑x : ℂ) * y) = cexp (log (-(↑x : ℂ)) * y + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₃ : cexp (log (↑x : ℂ) * y) = cexp ((log (-(↑x : ℂ)) + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₄ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑x : ℂ).arg : ℂ) * I) * y) = cexp ((log (-(↑x : ℂ)) + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₅ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑x : ℂ).arg : ℂ) * I) * y) =
  cexp (((↑(Real.log ‖-(↑x : ℂ)‖) : ℂ) + (↑(-(↑x : ℂ)).arg : ℂ) * I + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₆ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑x : ℂ).arg : ℂ) * I) * y) =
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(-(↑x : ℂ)).arg : ℂ) * I + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₇ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(-(↑x : ℂ)).arg : ℂ) * I + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₈ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑(↑(-x) : ℂ).arg : ℂ) * I + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₉ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑0 : ℂ) * I + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₁₀ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) =
  cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + 0 * I + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₁₁ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) = cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + 0 + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
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)
⊢ (↑x : ℂ) ^ y = (-(↑x : ℂ)) ^ y * cexp ((↑π : ℂ) * I * y)
have inr₁₂ : cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * I) * y) = cexp (((↑(Real.log ‖(↑x : ℂ)‖) : ℂ) + (↑π : ℂ) * 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
⊢ x ^ (↑y : ℂ) = (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)
have inl : HPow.hPow (α := ℂ) 0 (↑y : ℂ) =
  (↑(Norm.norm (E := ℂ) 0 ^ y) : ℂ) * ((↑(Real.cos (arg 0 * y)) : ℂ) + (↑(Real.sin (arg 0 * y)) : ℂ) * I)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
inl :
  HPow.hPow (α := ℂ) 0 (↑y : ℂ) =
    (↑(Norm.norm (E := ℂ) 0 ^ y) : ℂ) * ((↑(Real.cos (arg 0 * y)) : ℂ) + (↑(Real.sin (arg 0 * y)) : ℂ) * I)
⊢ x ^ (↑y : ℂ) = (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)
have inr : ∀ (hx : x ≠ 0), 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ (↑y : ℂ) = (↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)
have 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)
Tactic: rw [cpow_def_of_ne_zero hx, exp_eq_exp_re_mul_sin_add_cos, mul_comm (log x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ (↑(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)
have inr : 0 < ‖x‖
Tactic: rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul,
      Real.exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
y : ℝ
⊢ (x ^ (↑y : ℂ)).re = ‖x‖ ^ y * Real.cos (x.arg * y)
have rw : ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos (x.arg * y)) : ℂ) + (↑(Real.sin (x.arg * y)) : ℂ) * I)).re =
  ‖x‖ ^ y * Real.cos (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)).re =
    ‖x‖ ^ y * Real.cos (x.arg * y)
have generalize : ∀ (z : ℝ), ((↑(‖x‖ ^ y) : ℂ) * ((↑(Real.cos z) : ℂ) + (↑(Real.sin z) : ℂ) * I)).re = ‖x‖ ^ y * Real.cos z
Tactic: generalize arg x * y = z