awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
hx : ¬x = 0
rw : (if x = 0 then if Eq (α := ℂ) 1 0 then 1 else 0 else cexp (log x * 1)) = x
rw₁ : (if x = 0 then 0 else cexp (log x * 1)) = x
rw₂ : cexp (log x * 1) = x
rw₃ : cexp (log x) = x
rw₄ rw₅ : x = x
⊢ HPow.hPow (β := ℂ) x 1 = x

Tactic:
rw [cpow_def, if_neg (one_ne_zero : (1 : ℂ) ≠ 0), if_neg hx, mul_one, exp_log hx]

Premises used: Complex.cpow_def, mul_one, one_ne_zero, Complex.exp_log, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
pos : Eq (α := ℂ) 1 0 → x = 0 → Eq (α := ℂ) 1 1
neg : Eq (α := ℂ) 1 0 → ¬x = 0 → Eq (α := ℂ) 0 1
neg₁ : ¬Eq (α := ℂ) 1 0 → cexp (log 1 * x) = 1
⊢ (if Eq (α := ℂ) 1 0 then if x = 0 then 1 else 0 else cexp (log 1 * x)) = 1

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
h : Eq (α := ℂ) 1 0
h_1 : x = 0
⊢ Eq (α := ℂ) 1 1

Tactic:
simp_all [one_ne_zero]

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
h : Eq (α := ℂ) 1 0
h_1 : ¬x = 0
⊢ Eq (α := ℂ) 0 1

Tactic:
simp_all [one_ne_zero]

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
h : ¬Eq (α := ℂ) 1 0
⊢ cexp (log 1 * x) = 1

Tactic:
simp_all [one_ne_zero]

Premises used: one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
hx : x ≠ 0
simp :
  (if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then
        if x = 0 then if y = 0 then HMul.hMul (α := ℂ) 1 1 else HMul.hMul (α := ℂ) 0 1 else cexp (log x * y) * 1
      else if x = 0 then if y = 0 then HMul.hMul (α := ℂ) 1 0 else HMul.hMul (α := ℂ) 0 0 else cexp (log x * y) * 0
    else
      if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z)
      else cexp (log x * y) * cexp (log x * z)
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
simp only [cpow_def, ite_mul, mul_ite]

Premises used: mul_ite, ite_mul, Complex.cpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then
        if x = 0 then if y = 0 then HMul.hMul (α := ℂ) 1 1 else HMul.hMul (α := ℂ) 0 1 else cexp (log x * y) * 1
      else if x = 0 then if y = 0 then HMul.hMul (α := ℂ) 1 0 else HMul.hMul (α := ℂ) 0 0 else cexp (log x * y) * 0
    else
      if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z)
      else cexp (log x * y) * cexp (log x * z)

Tactic:
simp_all [exp_add, mul_add]

Premises used: Complex.exp_add, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
neg₉ : ¬x = 0 → ¬cexp (log x * y) = 0 → cexp (log x * (y * z)) = cexp (log (cexp (log x * y)) * z)
⊢ (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)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : y * z = 0
h_2 : y = 0
h_3 : Eq (α := ℂ) 1 0
h_4 : z = 0
⊢ Eq (α := ℂ) 1 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : y * z = 0
h_2 : y = 0
h_3 : Eq (α := ℂ) 1 0
h_4 : ¬z = 0
⊢ Eq (α := ℂ) 1 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : y * z = 0
h_2 : y = 0
h_3 : ¬Eq (α := ℂ) 1 0
⊢ 1 = cexp (log 1 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : y * z = 0
h_2 : ¬y = 0
h_3 : Eq (α := ℂ) 0 0
h_4 : z = 0
⊢ Eq (α := ℂ) 1 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : y * z = 0
h_2 : ¬y = 0
h_3 : Eq (α := ℂ) 0 0
h_4 : ¬z = 0
⊢ Eq (α := ℂ) 1 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : y * z = 0
h_2 : ¬y = 0
h_3 : ¬Eq (α := ℂ) 0 0
⊢ 1 = cexp (log 0 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : ¬y * z = 0
h_2 : y = 0
h_3 : Eq (α := ℂ) 1 0
h_4 : z = 0
⊢ Eq (α := ℂ) 0 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : ¬y * z = 0
h_2 : y = 0
h_3 : Eq (α := ℂ) 1 0
h_4 : ¬z = 0
⊢ Eq (α := ℂ) 0 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : ¬y * z = 0
h_2 : y = 0
h_3 : ¬Eq (α := ℂ) 1 0
⊢ 0 = cexp (log 1 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : ¬y * z = 0
h_2 : ¬y = 0
h_3 : Eq (α := ℂ) 0 0
h_4 : z = 0
⊢ Eq (α := ℂ) 0 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : ¬y * z = 0
h_2 : ¬y = 0
h_3 : Eq (α := ℂ) 0 0
h_4 : ¬z = 0
⊢ Eq (α := ℂ) 0 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : x = 0
h_1 : ¬y * z = 0
h_2 : ¬y = 0
h_3 : ¬Eq (α := ℂ) 0 0
⊢ 0 = cexp (log 0 * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : ¬x = 0
h_1 : cexp (log x * y) = 0
h_2 : z = 0
⊢ cexp (log x * (y * z)) = 1

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : ¬x = 0
h_1 : cexp (log x * y) = 0
h_2 : ¬z = 0
⊢ cexp (log x * (y * z)) = 0

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
h : ¬x = 0
h_1 : ¬cexp (log x * y) = 0
⊢ cexp (log x * (y * z)) = cexp (log (cexp (log x * y)) * z)

Tactic:
simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Premises used: Complex.exp_ne_zero, mul_assoc, Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
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))⁻¹
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
simp only [cpow_def, neg_eq_zero, mul_neg]

Premises used: neg_eq_zero, Complex.cpow_def, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
pos : x = 0 → y = 0 → Eq (α := ℂ) 1 1⁻¹
neg : x = 0 → ¬y = 0 → Eq (α := ℂ) 0 0⁻¹
neg₁ : ¬x = 0 → cexp (-(log x * y)) = (cexp (log 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))⁻¹

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
h : x = 0
h_1 : y = 0
⊢ Eq (α := ℂ) 1 1⁻¹

Tactic:
simp [exp_neg]

Premises used: Complex.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
h : x = 0
h_1 : ¬y = 0
⊢ Eq (α := ℂ) 0 0⁻¹

Tactic:
simp [exp_neg]

Premises used: Complex.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
h : ¬x = 0
⊢ cexp (-(log x * y)) = (cexp (log x * y))⁻¹

Tactic:
simp [exp_neg]

Premises used: Complex.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
rw₃ rw₄ : x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]

Premises used: sub_eq_add_neg, Complex.cpow_neg, div_eq_mul_inv, Complex.cpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
⊢ HPow.hPow (β := ℂ) x (-1) = x⁻¹

Tactic:
simpa using cpow_neg x 1

Premises used: Complex.cpow_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℤ
y : ℂ
inl : HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
inr : ∀ (hx : x ≠ 0), x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℤ
y : ℂ
inl : HPow.hPow (α := ℂ) 0 ((↑0 : ℂ) * y) = HPow.hPow (β := ℤ) (HPow.hPow (α := ℂ) 0 y) 0
inl₁ : ∀ (hn : n ≠ 0), HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
y : ℂ
⊢ HPow.hPow (α := ℂ) 0 ((↑0 : ℂ) * y) = HPow.hPow (β := ℤ) (HPow.hPow (α := ℂ) 0 y) 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℤ
y : ℂ
hn : n ≠ 0
inl : HPow.hPow (α := ℂ) 0 (HMul.hMul (α := ℂ) (↑n : ℂ) 0) = HPow.hPow (α := ℂ) (β := ℂ) 0 0 ^ n
inl₁ : ∀ (hy : y ≠ 0), HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℤ
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) 0 (HMul.hMul (α := ℂ) (↑n : ℂ) 0) = HPow.hPow (α := ℂ) (β := ℂ) 0 0 ^ n

Tactic:
simp [*, zero_zpow]

Premises used: zero_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℤ
y : ℂ
hn : n ≠ 0
hy : y ≠ 0
⊢ HPow.hPow (α := ℂ) 0 ((↑n : ℂ) * y) = HPow.hPow (α := ℂ) 0 y ^ n

Tactic:
simp [*, zero_zpow]

Premises used: zero_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
inr₃ inr₄ : cexp (log x * y) ^ n = cexp (log x * y) ^ n
⊢ 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]

Premises used: mul_left_comm, Complex.cpow_def_of_ne_zero, Complex.exp_int_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
n : ℤ
rw : x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
rw₁ rw₂ : (x ^ y) ^ n = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℂ)) = (x ^ y) ^ n

Tactic:
rw [mul_comm, cpow_int_mul]

Premises used: mul_comm, Complex.cpow_int_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
y : ℂ
⊢ x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n

Tactic:
mod_cast cpow_int_mul x n y

Premises used: zpow_natCast, Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, Nat.cast, HPow.hPow, congrFun', Complex.cpow_int_mul, Eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
inst : n.AtLeastTwo
y : ℂ
⊢ x ^ (OfNat.ofNat n * y) = HPow.hPow (β := ℕ) (x ^ y) (OfNat.ofNat n)

Tactic:
cpow_nat_mul x n y

Premises used: Complex.cpow_nat_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
n : ℕ
rw : x ^ ((↑n : ℂ) * y) = (x ^ y) ^ n
rw₁ rw₂ : (x ^ y) ^ n = (x ^ y) ^ n
⊢ x ^ (y * (↑n : ℂ)) = (x ^ y) ^ n

Tactic:
rw [mul_comm, cpow_nat_mul]

Premises used: Complex.cpow_nat_mul, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x y : ℂ
n : ℕ
inst : n.AtLeastTwo
⊢ x ^ (y * OfNat.ofNat n) = HPow.hPow (β := ℕ) (x ^ y) (OfNat.ofNat n)

Tactic:
cpow_mul_nat x y n

Premises used: Complex.cpow_mul_nat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
⊢ HPow.hPow (β := ℂ) x (↑n : ℂ) = x ^ n

Tactic:
simpa using cpow_nat_mul x n 1

Premises used: Complex.cpow_nat_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
inst : n.AtLeastTwo
⊢ HPow.hPow (β := ℂ) x (OfNat.ofNat n) = HPow.hPow (β := ℕ) x (OfNat.ofNat n)

Tactic:
cpow_natCast x n

Premises used: Complex.cpow_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
⊢ HPow.hPow (β := ℂ) x 2 = HPow.hPow (β := ℕ) x 2

Tactic:
cpow_ofNat x 2

Premises used: OfNat.ofNat, Complex.cpow_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℤ
⊢ HPow.hPow (β := ℂ) x (↑n : ℂ) = x ^ n

Tactic:
simpa using cpow_int_mul x n 1

Premises used: Complex.cpow_int_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
hn : n ≠ 0
rw : Ne (α := ℂ) (↑n : ℂ) 0
⊢ HPow.hPow (β := ℂ) x (↑n : ℂ)⁻¹ ^ n = x

Tactic:
rw [← cpow_nat_mul, mul_inv_cancel₀, cpow_one]

Premises used: mul_inv_cancel₀, Complex.cpow_nat_mul, Complex.cpow_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
hn : n ≠ 0
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ : ¬n = 0
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
assumption_mod_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
inst : n.AtLeastTwo
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℂ) x (OfNat.ofNat n)⁻¹) (OfNat.ofNat n) = x

Tactic:
cpow_nat_inv_pow _ (NeZero.ne n)

Premises used: Complex.cpow_nat_inv_pow, NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℤ
hlt : -π < (↑n : ℝ) * x.arg
hle : (↑n : ℝ) * x.arg ≤ π
y : ℂ
rw : ∀ (hlt : -π < x.arg * (↑n : ℝ)) (hle : x.arg * (↑n : ℝ) ≤ π) (y : ℂ), x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y
⊢ x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y

Tactic:
rw [mul_comm] at hlt hle

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℤ
hlt : -π < x.arg * (↑n : ℝ)
hle : x.arg * (↑n : ℝ) ≤ π
y : ℂ
h₁ : -π < (log x * (↑n : ℂ)).im
h₂ : (log x * (↑n : ℂ)).im ≤ π
⊢ x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y

Tactic:
rw [cpow_mul, cpow_intCast]

Premises used: Complex.cpow_intCast, Complex.cpow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℤ
hlt : -π < x.arg * (↑n : ℝ)
hle : x.arg * (↑n : ℝ) ≤ π
y : ℂ
⊢ -π < (log x * (↑n : ℂ)).im

Tactic:
simpa [log_im]

Premises used: Complex.log_im
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℤ
hlt : -π < x.arg * (↑n : ℝ)
hle : x.arg * (↑n : ℝ) ≤ π
y : ℂ
⊢ (log x * (↑n : ℂ)).im ≤ π

Tactic:
simpa [log_im]

Premises used: Complex.log_im
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
hlt : -π < (↑n : ℝ) * x.arg
hle : (↑n : ℝ) * x.arg ≤ π
y : ℂ
⊢ x ^ ((↑n : ℂ) * y) = (x ^ n) ^ y

Tactic:
cpow_int_mul' hlt hle y

Premises used: zpowRec, Complex.cpow_int_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
inst : n.AtLeastTwo
hlt : -π < OfNat.ofNat n * x.arg
hle : OfNat.ofNat n * x.arg ≤ π
y : ℂ
⊢ x ^ (OfNat.ofNat n * y) = HPow.hPow (β := ℕ) x (OfNat.ofNat n) ^ y

Tactic:
cpow_nat_mul' hlt hle y

Premises used: Complex.cpow_nat_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / (↑n : ℝ)) < x.arg
hle : x.arg ≤ π / (↑n : ℝ)
hlt₁ : -π < (↑n : ℝ) * x.arg
hle₁ : (↑n : ℝ) * x.arg ≤ π
⊢ HPow.hPow (β := ℂ) (x ^ n) (↑n : ℂ)⁻¹ = x

Tactic:
rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one]

Premises used: mul_inv_cancel₀, Complex.cpow_one, Complex.cpow_nat_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / (↑n : ℝ)) < x.arg
hle : x.arg ≤ π / (↑n : ℝ)
hlt₁ : -π / (↑n : ℝ) < x.arg
hlt₂ hlt₃ hlt₄ hlt₅ : -(π / (↑n : ℝ)) < x.arg
⊢ -π < (↑n : ℝ) * x.arg

Tactic:
rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div]

Premises used: neg_div, div_lt_iff₀'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / (↑n : ℝ)) < x.arg
hle : x.arg ≤ π / (↑n : ℝ)
hle₁ hle₂ hle₃ hle₄ : x.arg ≤ π / (↑n : ℝ)
⊢ (↑n : ℝ) * x.arg ≤ π

Tactic:
rwa [← le_div_iff₀' (Nat.cast_pos.2 h₀.bot_lt)]

Premises used: le_div_iff₀'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
n : ℕ
inst : n.AtLeastTwo
hlt : -(π / OfNat.ofNat n) < x.arg
hle : x.arg ≤ π / OfNat.ofNat n
⊢ HPow.hPow (β := ℂ) (HPow.hPow (β := ℕ) x (OfNat.ofNat n)) (OfNat.ofNat n)⁻¹ = x

Tactic:
pow_cpow_nat_inv (NeZero.ne n) hlt hle

Premises used: Complex.pow_cpow_nat_inv, NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
hx : 0 < x.re
⊢ HPow.hPow (β := ℂ) (HPow.hPow (β := ℕ) x 2) 2⁻¹ = x

Tactic:
pow_cpow_ofNat_inv (neg_pi_div_two_lt_arg_iff.2 <| .inl hx)
    (arg_le_pi_div_two_iff.2 <| .inl hx.le)

Premises used: Iff.mpr, Complex.neg_pi_div_two_lt_arg_iff, Complex.arg_le_pi_div_two_iff, LT.lt.le, Complex.pow_cpow_ofNat_inv, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x : ℂ
⊢ x = HPow.hPow (β := ℂ) x 2⁻¹ * HPow.hPow (β := ℂ) x 2⁻¹

Tactic:
simp [← sq]

Premises used: sq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
inl : HPow.hPow (β := ℂ) ((↑a : ℂ) * (↑b : ℂ)) 0 = HPow.hPow (β := ℂ) (↑a : ℂ) 0 * HPow.hPow (β := ℂ) (↑b : ℂ) 0
inr : ∀ (hr : r ≠ 0), ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ HPow.hPow (β := ℂ) ((↑a : ℂ) * (↑b : ℂ)) 0 = HPow.hPow (β := ℂ) (↑a : ℂ) 0 * HPow.hPow (β := ℂ) (↑b : ℂ) 0

Tactic:
simp only [cpow_zero, mul_one]

Premises used: mul_one, Complex.cpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
inr₁ : ∀ (ha' : 0 < a), ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r

Tactic:
rcases eq_or_lt_of_le ha with (rfl | ha')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
inr₃ inr₄ : Eq (α := ℂ) 0 0
⊢ ((↑0 : ℂ) * (↑b : ℂ)) ^ r = (↑0 : ℂ) ^ r * (↑b : ℂ) ^ r

Tactic:
rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]

Premises used: MulZeroClass.zero_mul, Complex.zero_cpow, Complex.ofReal_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
inr₁ : ∀ (hb' : 0 < b), ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑a : ℂ) * (↑b : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r

Tactic:
rcases eq_or_lt_of_le hb with (rfl | hb')

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
inr₃ inr₄ : Eq (α := ℂ) 0 0
⊢ ((↑a : ℂ) * (↑0 : ℂ)) ^ r = (↑a : ℂ) ^ r * (↑0 : ℂ) ^ r

Tactic:
rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]

Premises used: MulZeroClass.mul_zero, Complex.zero_cpow, Complex.ofReal_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
⊢ (↑a : ℂ) ≠ 0

Tactic:
have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : (↑a : ℂ) ≠ 0
⊢ (↑b : ℂ) ≠ 0

Tactic:
have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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
inr₆ inr₇ : (↑a : ℂ) ^ r * (↑b : ℂ) ^ r = (↑a : ℂ) ^ r * (↑b : ℂ) ^ r
⊢ ((↑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'']

Premises used: add_mul, Complex.exp_add, Complex.ofReal_log, Complex.log_ofReal_mul, mul_ne_zero, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
m n : ℕ
s : ℂ
⊢ HMul.hMul (α := ℂ) (↑m : ℂ) (↑n : ℂ) ^ s = HPow.hPow (α := ℂ) (↑m : ℂ) s * HPow.hPow (α := ℂ) (↑n : ℂ) s

Tactic:
ofReal_natCast m ▸ ofReal_natCast n ▸ mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg s

Premises used: Nat.cast_nonneg, Eq.rec, Complex.mul_cpow_ofReal_nonneg, Complex.ofReal_natCast