awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
pos₃ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 0 1
neg₆ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₇ : x = 0 → ¬y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 0 = cexp (log 0 * z)
pos₄ : ¬x = 0 → cexp (log x * y) = 0 → z = 0 → cexp (log x * (y * z)) = 1
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₈ : ¬x = 0 → cexp (log x * y) = 0 → ¬z = 0 → cexp (log x * (y * z)) = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
pos : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 1 1
neg : x = 0 → y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₁ : x = 0 → y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 1 = cexp (log 1 * z)
pos₁ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 1 1
neg₂ : x = 0 → y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 1 0
neg₃ : x = 0 → y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 1 = cexp (log 0 * z)
pos₂ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → z = 0 → Eq (α := ℂ) 0 1
neg₄ : x = 0 → ¬y * z = 0 → y = 0 → Eq (α := ℂ) 1 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₅ : x = 0 → ¬y * z = 0 → y = 0 → ¬Eq (α := ℂ) 1 0 → 0 = cexp (log 1 * z)
pos₃ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → z = 0 → Eq (α := ℂ) 0 1
neg₆ : x = 0 → ¬y * z = 0 → ¬y = 0 → Eq (α := ℂ) 0 0 → ¬z = 0 → Eq (α := ℂ) 0 0
neg₇ : x = 0 → ¬y * z = 0 → ¬y = 0 → ¬Eq (α := ℂ) 0 0 → 0 = cexp (log 0 * z)
pos₄ : ¬x = 0 → cexp (log x * y) = 0 → z = 0 → cexp (log x * (y * z)) = 1
neg₈ : ¬x = 0 → cexp (log x * y) = 0 → ¬z = 0 → cexp (log x * (y * z)) = 0
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
have neg₉ : ¬x = 0 → ¬cexp (log x * y) = 0 → cexp (log x * (y * z)) = cexp (log (cexp (log x * y)) * z)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹
have simp : (if x = 0 then if y = 0 then 1 else 0 else cexp (-(log x * y))) =
  (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y))⁻¹
Tactic: simp only [cpow_def, neg_eq_zero, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (-(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 → Eq (α := ℂ) 1 1⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
pos : x = 0 → y = 0 → Eq (α := ℂ) 1 1⁻¹
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (-(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 → Eq (α := ℂ) 0 0⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
pos : x = 0 → y = 0 → Eq (α := ℂ) 1 1⁻¹
neg : x = 0 → ¬y = 0 → Eq (α := ℂ) 0 0⁻¹
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (-(log x * y))) =
    (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y))⁻¹
have neg₁ : ¬x = 0 → cexp (-(log x * y)) = (cexp (log x * y))⁻¹
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw : x ^ (y + -z) = x ^ y / x ^ z
Tactic: rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
hx : x ≠ 0
rw : x ^ (y + -z) = x ^ y / x ^ z
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw₁ : x ^ y * x ^ (-z) = x ^ y / x ^ z
Tactic: rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
hx : x ≠ 0
rw : x ^ (y + -z) = x ^ y / x ^ z
rw₁ : x ^ y * x ^ (-z) = x ^ y / x ^ z
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw₂ : x ^ y * (x ^ z)⁻¹ = x ^ y / x ^ z
Tactic: rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y z : ℂ
hx : x ≠ 0
rw : x ^ (y + -z) = x ^ y / x ^ z
rw₁ : x ^ y * x ^ (-z) = x ^ y / x ^ z
rw₂ : x ^ y * (x ^ z)⁻¹ = x ^ y / x ^ z
⊢ x ^ (y - z) = x ^ y / x ^ z
have rw₃ : x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹
Tactic: rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
y : ℂ
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
have inl : HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
y : ℂ
inl : HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
have inr : ∀ (hx : x ≠ 0), x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
n : ℤ
y : ℂ
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
have inl : HPow.hPow (α := ℂ) 0 ((↑0 : ℂ) * y) = HPow.hPow (β := ℤ) (HPow.hPow (α := ℂ) 0 y) 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
n : ℤ
y : ℂ
inl : HPow.hPow (α := ℂ) 0 ((↑0 : ℂ) * y) = HPow.hPow (β := ℤ) (HPow.hPow (α := ℂ) 0 y) 0
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
have inl₁ : ∀ (hn : n ≠ 0), HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
have inl : HPow.hPow (α := ℂ) 0 (HMul.hMul (α := ℂ) (↑n : ℂ) 0) = HPow.hPow (α := ℂ) (β := ℂ) 0 0 ^ n
Tactic: rcases eq_or_ne y 0 with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
n : ℤ
y : ℂ
hn : n ≠ 0
inl : HPow.hPow (α := ℂ) 0 (HMul.hMul (α := ℂ) (↑n : ℂ) 0) = HPow.hPow (α := ℂ) (β := ℂ) 0 0 ^ n
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
have inl₁ : ∀ (hy : y ≠ 0), HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
Tactic: rcases eq_or_ne y 0 with rfl | hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
have inr : cexp (log x * ((↑n : ℂ) * y)) = (x ^ y) ^ n
Tactic: rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
inr : cexp (log x * ((↑n : ℂ) * y)) = (x ^ y) ^ n
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
have inr₁ : cexp (log x * ((↑n : ℂ) * y)) = cexp (log x * y) ^ n
Tactic: rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
inr : cexp (log x * ((↑n : ℂ) * y)) = (x ^ y) ^ n
inr₁ : cexp (log x * ((↑n : ℂ) * y)) = cexp (log x * y) ^ n
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
have inr₂ : cexp ((↑n : ℂ) * (log x * y)) = cexp (log x * y) ^ n
Tactic: rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
inr : cexp (log x * ((↑n : ℂ) * y)) = (x ^ y) ^ n
inr₁ : cexp (log x * ((↑n : ℂ) * y)) = cexp (log x * y) ^ n
inr₂ : cexp ((↑n : ℂ) * (log x * y)) = cexp (log x * y) ^ n
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
have inr₃ : cexp (log x * y) ^ n = cexp (log x * y) ^ n
Tactic: rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
n : ℤ
⊢ x ^ (y * (↑n : ℂ)) = (x ^ y) ^ n
have rw : x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
Tactic: rw [mul_comm, cpow_int_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
n : ℤ
rw : x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℂ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [mul_comm, cpow_int_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
n : ℕ
⊢ x ^ (y * (↑n : ℂ)) = (x ^ y) ^ n
have rw : x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
Tactic: rw [mul_comm, cpow_nat_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x y : ℂ
n : ℕ
rw : x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℂ)) = (x ^ y) ^ n
have rw₁ : (x ^ y) ^ n = (x ^ y) ^ n
Tactic: rw [mul_comm, cpow_nat_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹ ^ n = x
have rw : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: rw [← cpow_nat_mul, mul_inv_cancel₀, cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℕ
hn : n ≠ 0
⊢ Ne (α := ℂ) (↑n : ℂ) 0
have assumption_mod_cast : ¬n = 0
Tactic: assumption_mod_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
hlt : -π < (↑n : ℝ) * x.arg
hle : (↑n : ℝ) * x.arg ≤ π
y : ℂ
⊢ x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y
have rw : ∀ (hlt : -π < x.arg * (↑n : ℝ)) (hle : x.arg * (↑n : ℝ) ≤ π) (y : ℂ), x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y
Tactic: rw [mul_comm] at hlt hle
Cleared hypotheses: hlt, hle, y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
hlt : -π < x.arg * (↑n : ℝ)
hle : x.arg * (↑n : ℝ) ≤ π
y : ℂ
⊢ x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y
have h₁ : -π < (log x * (↑n : ℂ)).im
Tactic: rw [cpow_mul, cpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℤ
hlt : -π < x.arg * (↑n : ℝ)
hle : x.arg * (↑n : ℝ) ≤ π
y : ℂ
h₁ : -π < (log x * (↑n : ℂ)).im
⊢ x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y
have h₂ : (log x * (↑n : ℂ)).im ≤ π
Tactic: rw [cpow_mul, cpow_intCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / (↑n : ℝ)) < x.arg
hle : x.arg ≤ π / (↑n : ℝ)
⊢ HPow.hPow (β := ℂ) (x ^ n) (↑n : ℂ)⁻¹ = x
have hlt₁ : -π < (↑n : ℝ) * x.arg
Tactic: rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / (↑n : ℝ)) < x.arg
hle : x.arg ≤ π / (↑n : ℝ)
hlt₁ : -π < (↑n : ℝ) * x.arg
⊢ HPow.hPow (β := ℂ) (x ^ n) (↑n : ℂ)⁻¹ = x
have hle₁ : (↑n : ℝ) * x.arg ≤ π
Tactic: rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / (↑n : ℝ)) < x.arg
hle : x.arg ≤ π / (↑n : ℝ)
⊢ -π < (↑n : ℝ) * x.arg
have hlt₁ : -π / (↑n : ℝ) < x.arg
Tactic: rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inl : HPow.hPow (β := ℂ) ((↑a : ℂ) * (↑b : ℂ)) 0 = HPow.hPow (β := ℂ) (↑a : ℂ) 0 * HPow.hPow (β := ℂ) (↑b : ℂ) 0
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
inl : HPow.hPow (β := ℂ) ((↑a : ℂ) * (↑b : ℂ)) 0 = HPow.hPow (β := ℂ) (↑a : ℂ) 0 * HPow.hPow (β := ℂ) (↑b : ℂ) 0
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr : ∀ (hr : r ≠ 0), ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr : ∀ (ha : LE.le (α := ℝ) 0 0), ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rcases eq_or_lt_of_le ha with (rfl | ha')
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
inr : ∀ (ha : LE.le (α := ℝ) 0 0), ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₁ : ∀ (ha' : 0 < a), ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rcases eq_or_lt_of_le ha with (rfl | ha')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : LE.le (α := ℝ) 0 0
⊢ ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r
have inr : (0 * (↑b : ℂ)) ^ r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
Tactic: rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : LE.le (α := ℝ) 0 0
inr : (0 * (↑b : ℂ)) ^ r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
⊢ ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₁ : HPow.hPow (α := ℂ) 0 r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
Tactic: rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : LE.le (α := ℝ) 0 0
inr : (0 * (↑b : ℂ)) ^ r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
inr₁ : HPow.hPow (α := ℂ) 0 r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
⊢ ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₂ : 0 = 0 * (↑b : ℂ) ^ r
Tactic: rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : LE.le (α := ℝ) 0 0
inr : (0 * (↑b : ℂ)) ^ r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
inr₁ : HPow.hPow (α := ℂ) 0 r = HPow.hPow (α := ℂ) 0 r * (↑b : ℂ) ^ r
inr₂ : 0 = 0 * (↑b : ℂ) ^ r
⊢ ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₃ : Eq (α := ℂ) 0 0
Tactic: rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr : ∀ (hb : LE.le (α := ℝ) 0 0), ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r
Tactic: rcases eq_or_lt_of_le hb with (rfl | hb')
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
inr : ∀ (hb : LE.le (α := ℝ) 0 0), ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₁ : ∀ (hb' : 0 < b), ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rcases eq_or_lt_of_le hb with (rfl | hb')
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : LE.le (α := ℝ) 0 0
⊢ ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r
have inr : ((↑a : ℂ) * 0) ^ r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
Tactic: rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : LE.le (α := ℝ) 0 0
inr : ((↑a : ℂ) * 0) ^ r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
⊢ ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r
have inr₁ : HPow.hPow (α := ℂ) 0 r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
Tactic: rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : LE.le (α := ℝ) 0 0
inr : ((↑a : ℂ) * 0) ^ r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
inr₁ : HPow.hPow (α := ℂ) 0 r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
⊢ ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r
have inr₂ : 0 = (↑a : ℂ) ^ r * 0
Tactic: rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : LE.le (α := ℝ) 0 0
inr : ((↑a : ℂ) * 0) ^ r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
inr₁ : HPow.hPow (α := ℂ) 0 r = (↑a : ℂ) ^ r * HPow.hPow (α := ℂ) 0 r
inr₂ : 0 = (↑a : ℂ) ^ r * 0
⊢ ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r
have inr₃ : Eq (α := ℂ) 0 0
Tactic: rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (hypothesis)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have ha'' : (↑a : ℂ) ≠ 0
Tactic: have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (hypothesis)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have hb'' : (↑b : ℂ) ≠ 0
Tactic: have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₁ : cexp (((↑(Real.log a) : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₁ : cexp (((↑(Real.log a) : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₂ : cexp ((log (↑a : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₁ : cexp (((↑(Real.log a) : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₂ : cexp ((log (↑a : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₃ : cexp (log (↑a : ℂ) * r + log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₁ : cexp (((↑(Real.log a) : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₂ : cexp ((log (↑a : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₃ : cexp (log (↑a : ℂ) * r + log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₄ : cexp (log (↑a : ℂ) * r) * cexp (log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₁ : cexp (((↑(Real.log a) : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₂ : cexp ((log (↑a : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₃ : cexp (log (↑a : ℂ) * r + log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₄ : cexp (log (↑a : ℂ) * r) * cexp (log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₅ : (↑a : ℂ) ^ r * cexp (log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
hb'' : (↑b : ℂ) ≠ 0
inr : cexp (log ((↑a : ℂ) * (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₁ : cexp (((↑(Real.log a) : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₂ : cexp ((log (↑a : ℂ) + log (↑b : ℂ)) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₃ : cexp (log (↑a : ℂ) * r + log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₄ : cexp (log (↑a : ℂ) * r) * cexp (log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
inr₅ : (↑a : ℂ) ^ r * cexp (log (↑b : ℂ) * r) = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
have inr₆ : (↑a : ℂ) ^ r * (↑b : ℂ) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
Tactic: rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
    add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
n m : ℕ
z : ℂ
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) ((↑m : ℂ) * z) = HPow.hPow (α := ℂ) (↑n : ℂ) m ^ z
have refine_1 : -π < (↑m : ℝ) * arg (↑n : ℂ)
Tactic: refine cpow_nat_mul' (x := n) (n := m) ?_ ?_ z