awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
n m : ℕ
z : ℂ
refine_1 : -π < (↑m : ℝ) * arg (↑n : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) ((↑m : ℂ) * z) = HPow.hPow (α := ℂ) (↑n : ℂ) m ^ z
have refine_2 : (↑m : ℝ) * arg (↑n : ℂ) ≤ π
Tactic: refine cpow_nat_mul' (x := n) (n := m) ?_ ?_ z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
⊢ x⁻¹ ^ n =
    if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
    else (x ^ n)⁻¹
have simp_rw : (if x = 0 then if n = 0 then 1 else 0
  else
    if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else (cexp (log x * n))⁻¹) =
  if x.arg = π then
    if x = 0 then if n = 0 then 1 else 0
    else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
  else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
Tactic: simp_rw [Complex.cpow_def, log_inv_eq_ite, inv_eq_zero, map_eq_zero, ite_mul, neg_mul,
    RCLike.conj_inv, apply_ite conj, apply_ite exp, apply_ite Inv.inv, map_zero, map_one, exp_neg,
    inv_one, inv_zero, ← exp_conj, map_mul, conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else
      if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
      else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0
      else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
have pos : ∀ (hx : x = 0) (hn : n = 0) (ha : x.arg = π), Eq (α := ℂ) 1 1
Tactic: split_ifs with hx hn ha ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hx : x = 0) (hn : n = 0) (ha : x.arg = π), Eq (α := ℂ) 1 1
⊢ (if x = 0 then if n = 0 then 1 else 0
    else
      if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
      else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0
      else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
have neg : ∀ (hx : x = 0) (hn : n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 1 1
Tactic: split_ifs with hx hn ha ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hx : x = 0) (hn : n = 0) (ha : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hx : x = 0) (hn : n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 1 1
⊢ (if x = 0 then if n = 0 then 1 else 0
    else
      if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
      else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0
      else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
have pos₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : x.arg = π), Eq (α := ℂ) 0 0
Tactic: split_ifs with hx hn ha ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hx : x = 0) (hn : n = 0) (ha : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hx : x = 0) (hn : n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 1 1
pos₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : x.arg = π), Eq (α := ℂ) 0 0
⊢ (if x = 0 then if n = 0 then 1 else 0
    else
      if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
      else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0
      else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
have neg₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 0 0
Tactic: split_ifs with hx hn ha ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hx : x = 0) (hn : n = 0) (ha : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hx : x = 0) (hn : n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 1 1
pos₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : x.arg = π), Eq (α := ℂ) 0 0
neg₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 0 0
⊢ (if x = 0 then if n = 0 then 1 else 0
    else
      if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
      else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0
      else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
have pos₂ : ∀ (hx : ¬x = 0),
  x.arg = π →
    (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹ =
      (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
Tactic: split_ifs with hx hn ha ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hx : x = 0) (hn : n = 0) (ha : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hx : x = 0) (hn : n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 1 1
pos₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : x.arg = π), Eq (α := ℂ) 0 0
neg₁ : ∀ (hx : x = 0) (hn : ¬n = 0) (ha : ¬x.arg = π), Eq (α := ℂ) 0 0
pos₂ :
  ∀ (hx : ¬x = 0),
    x.arg = π →
      (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹ =
        (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
⊢ (if x = 0 then if n = 0 then 1 else 0
    else
      if x.arg = π then (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
      else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1 else 0
      else (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
have neg₂ : ∀ (hx : ¬x = 0), ¬x.arg = π → (cexp (log x * n))⁻¹ = (cexp (log x * n))⁻¹
Tactic: split_ifs with hx hn ha ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
hx : x.arg ≠ π
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
have rw : (if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
  else (x ^ n)⁻¹) =
  (x ^ n)⁻¹
Tactic: rw [inv_cpow_eq_ite, if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
hx : x.arg ≠ π
rw :
  (if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
    else (x ^ n)⁻¹) =
    (x ^ n)⁻¹
⊢ x⁻¹ ^ n = (x ^ n)⁻¹
have rw₁ : (x ^ n)⁻¹ = (x ^ n)⁻¹
Tactic: rw [inv_cpow_eq_ite, if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
⊢ (x ^ n)⁻¹ =
    if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x⁻¹ ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
    else x⁻¹ ^ n
have rw : (x ^ n)⁻¹ =
  if x.arg = π then
    if x.arg = π then (x ^ n)⁻¹
    else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
  else x⁻¹ ^ n
Tactic: rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
⊢ (x ^ n)⁻¹ =
    if x.arg = π then
      if x.arg = π then (x ^ n)⁻¹
      else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
    else x⁻¹ ^ n
have pos : ∀ (h : x.arg = π), (x ^ n)⁻¹ = (x ^ n)⁻¹
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (h : x.arg = π), (x ^ n)⁻¹ = (x ^ n)⁻¹
⊢ (x ^ n)⁻¹ =
    if x.arg = π then
      if x.arg = π then (x ^ n)⁻¹
      else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
    else x⁻¹ ^ n
have neg : ∀ (h : ¬x.arg = π), (x ^ n)⁻¹ = x⁻¹ ^ n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
have neg : (x ^ n)⁻¹ = (x ^ n)⁻¹
Tactic: rw [inv_cpow _ _ h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n =
    if x.arg = π then x ^ n
    else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
have simp_rw : (if x = 0 then if n = 0 then 1 else 0
  else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
  if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
  else if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
Tactic: simp_rw [cpow_def, map_eq_zero, apply_ite conj, map_one, map_zero, ← exp_conj, map_mul, conj_conj,
    log_conj_eq_ite]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
have pos : ∀ (hcx : x = 0) (hn : n = 0) (hx : x.arg = π), Eq (α := ℂ) 1 1
Tactic: split_ifs with hcx hn hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hcx : x = 0) (hn : n = 0) (hx : x.arg = π), Eq (α := ℂ) 1 1
⊢ (if x = 0 then if n = 0 then 1 else 0
    else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
have neg : ∀ (hcx : x = 0) (hn : n = 0) (hx : ¬x.arg = π), Eq (α := ℂ) 1 1
Tactic: split_ifs with hcx hn hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hcx : x = 0) (hn : n = 0) (hx : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hcx : x = 0) (hn : n = 0) (hx : ¬x.arg = π), Eq (α := ℂ) 1 1
⊢ (if x = 0 then if n = 0 then 1 else 0
    else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
have pos₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), x.arg = π → Eq (α := ℂ) 0 0
Tactic: split_ifs with hcx hn hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hcx : x = 0) (hn : n = 0) (hx : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hcx : x = 0) (hn : n = 0) (hx : ¬x.arg = π), Eq (α := ℂ) 1 1
pos₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), x.arg = π → Eq (α := ℂ) 0 0
⊢ (if x = 0 then if n = 0 then 1 else 0
    else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
have neg₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), ¬x.arg = π → Eq (α := ℂ) 0 0
Tactic: split_ifs with hcx hn hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hcx : x = 0) (hn : n = 0) (hx : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hcx : x = 0) (hn : n = 0) (hx : ¬x.arg = π), Eq (α := ℂ) 1 1
pos₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), x.arg = π → Eq (α := ℂ) 0 0
neg₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), ¬x.arg = π → Eq (α := ℂ) 0 0
⊢ (if x = 0 then if n = 0 then 1 else 0
    else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
have pos₂ : ∀ (hcx : ¬x = 0), x.arg = π → cexp (log x * n) = cexp (log x * n)
Tactic: split_ifs with hcx hn hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
pos : ∀ (hcx : x = 0) (hn : n = 0) (hx : x.arg = π), Eq (α := ℂ) 1 1
neg : ∀ (hcx : x = 0) (hn : n = 0) (hx : ¬x.arg = π), Eq (α := ℂ) 1 1
pos₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), x.arg = π → Eq (α := ℂ) 0 0
neg₁ : ∀ (hcx : x = 0) (hn : ¬n = 0), ¬x.arg = π → Eq (α := ℂ) 0 0
pos₂ : ∀ (hcx : ¬x = 0), x.arg = π → cexp (log x * n) = cexp (log x * n)
⊢ (if x = 0 then if n = 0 then 1 else 0
    else cexp ((if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else
      if x = 0 then if n = 0 then 1 else 0 else cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
have neg₂ : ∀ (hcx : ¬x = 0),
  ¬x.arg = π →
    cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n) =
      cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)
Tactic: split_ifs with hcx hn hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
hx : x.arg ≠ π
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
have rw : (if x.arg = π then x ^ n
  else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
Tactic: rw [conj_cpow_eq_ite, if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
hx : x.arg ≠ π
rw :
  (if x.arg = π then x ^ n
    else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
have rw₁ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)) : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)) : ℂ)
Tactic: rw [conj_cpow_eq_ite, if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
hx : x.arg ≠ π
⊢ HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
have rw : HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)) : ℂ)
Tactic: rw [conj_cpow _ _ hx, conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (goal)
Goal:
x n : ℂ
hx : x.arg ≠ π
rw :
  HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)) : ℂ)
⊢ HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)
have rw₁ : HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) = HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)
Tactic: rw [conj_cpow _ _ hx, conj_conj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Complex (hypothesis)
Goal:
n : ℕ
z : ℂ
H : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0 ∧ z ≠ 0
⊢ False
have H₁ : False ∧ ¬z = 0
Tactic: norm_cast at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ HPow.hPow (α := ℂ) 0 x = 0 x
have rw : Eq (α := ℂ) 0 (0 x)
Tactic: rw [zero_cpow hx, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
rw : Eq (α := ℂ) 0 (0 x)
⊢ HPow.hPow (α := ℂ) 0 x = 0 x
have rw₁ : Eq (α := ℂ) 0 0
Tactic: rw [zero_cpow hx, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
b : ℂ
hb : b ≠ 0
⊢ (𝓝 b).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ HPow.hPow (α := ℂ) 0 x) 0
have suffices : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
Tactic: suffices ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [zero_cpow hx, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ x ^ b = cexp (Complex.log x * b)
have rw : cexp (Complex.log x * b) = cexp (Complex.log x * b)
Tactic: rw [cpow_def_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
ha : a ≠ 0
⊢ (𝓝 a).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ x ^ b) fun (x : ℂ) ↦ cexp (Complex.log x * b)
have suffices : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
Tactic: suffices ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [cpow_def_of_ne_zero hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)
have suffices : IsOpen (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}ᶜ
Tactic: suffices IsOpen {x : ℂ × ℂ | x.1 = 0}ᶜ from
    mem_nhds_iff.mpr ⟨_, fun x hx ↦ by simp_all [cpow_def_of_ne_zero], this, hp_fst⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsOpen (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}ᶜ
have rw : IsClosed (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}
Tactic: rw [isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
ha : a ≠ 0
⊢ Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ a ^ x) fun (x : ℂ) ↦ cexp (Complex.log a * x)
have h : ∀ (b : ℂ), a ^ b = cexp (Complex.log a * b)
Tactic: ext1 b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b_1 : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = cexp (Complex.log a * b)
have h : cexp (Complex.log a * b) = cexp (Complex.log a * b)
Tactic: rw [cpow_def_of_ne_zero ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
a b : ℂ
ha : a ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
have cpow_eq : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ a ^ x) fun (x : ℂ) ↦ cexp (Complex.log a * x)
Tactic: have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) := by
    ext1 b
    rw [cpow_def_of_ne_zero ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
ha : a ≠ 0
cpow_eq : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ a ^ x) fun (x : ℂ) ↦ cexp (Complex.log a * x)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
have rw : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ cexp (Complex.log a * x)) b
Tactic: rw [cpow_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
h : b ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
have pos : ∀ (ha : a = 0), ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
h : b ≠ 0
pos : ∀ (ha : a = 0), ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
have neg : ∀ (ha : ¬a = 0), ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
have pos : ContinuousAt (Y := ℂ) 0 b
Tactic: rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) p
have rw : ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)) p
Tactic: rw [continuousAt_congr (cpow_eq_nhds' <| slitPlane_ne_zero hp_fst)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)) p
have refine : ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ Complex.log x.1 * x.2) p
Tactic: refine continuous_exp.continuousAt.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))
have inl : ∀ (h : a ≠ 0), Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))
Tactic: cases h with
  | inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
  | inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
inl : ∀ (h : a ≠ 0), Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))
⊢ Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))
have inr : ∀ (h : b ≠ 0), Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))
Tactic: cases h with
  | inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
  | inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ ((↑a : ℂ) ^ (↑x : ℂ)).re) b
have refine : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b
Tactic: refine Complex.continuous_re.continuousAt.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b
have refine : (↑a : ℂ) ≠ 0
Tactic: refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℝ
h : a ≠ 0
⊢ (↑a : ℂ) ≠ 0
have norm_cast : ¬a = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ ((↑a : ℂ) ^ (↑x : ℂ)).re) b
have refine : ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b
Tactic: refine Complex.continuous_re.continuousAt.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑a : ℂ) ^ (↑x : ℂ)) b
have refine : (↑b : ℂ) ≠ 0
Tactic: refine (continuousAt_const_cpow' ?_).comp Complex.continuous_ofReal.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
a b : ℝ
h : b ≠ 0
⊢ (↑b : ℂ) ≠ 0
have norm_cast : ¬b = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2) * cos (x.2 * π)
have rw : rexp (log x.1 * x.2) * cos (x.2 * π) = rexp (log x.1 * x.2) * cos (x.2 * π)
Tactic: rw [rpow_def_of_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp_fst : p.1 < 0
⊢ (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
have suffices : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
Tactic: suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, x.1 < 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [rpow_def_of_neg hx]