awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n m : ℕ
z : ℂ
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) ((↑m : ℂ) * z) = HPow.hPow (α := ℂ) (↑n : ℂ) m ^ z

Tactic:
cpow_nat_mul' (x := n) (n := m) ?_ ?_ z

Premises used: Complex.cpow_nat_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n m : ℕ
z : ℂ
refine_1 : -π < (↑m : ℝ) * arg (↑n : ℂ)
refine_2 : (↑m : ℝ) * arg (↑n : ℂ) ≤ π
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) ((↑m : ℂ) * z) = HPow.hPow (α := ℂ) (↑n : ℂ) m ^ z

Tactic:
refine cpow_nat_mul' (x := n) (n := m) ?_ ?_ z

Premises used: Complex.cpow_nat_mul'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n m : ℕ
z : ℂ
⊢ -π < (↑m : ℝ) * arg (↑n : ℂ)

Tactic:
simp only [natCast_arg, mul_zero, Left.neg_neg_iff, pi_pos]

Premises used: Left.neg_neg_iff, Real.pi_pos, MulZeroClass.mul_zero, Complex.natCast_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n m : ℕ
z : ℂ
⊢ (↑m : ℝ) * arg (↑n : ℂ) ≤ π

Tactic:
simp only [natCast_arg, mul_zero, pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le, MulZeroClass.mul_zero, Complex.natCast_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
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))⁻¹
⊢ x⁻¹ ^ n =
    if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
    else (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]

Premises used: inv_eq_zero, inv_one, Complex.log_inv_eq_ite, inv_zero, apply_ite, map_zero, Complex.exp_neg, map_eq_zero, map_mul, Inv.inv, map_one, ite_mul, Complex.exp_conj, Complex.conj_conj, Complex.exp, Complex.cpow_def, RCLike.conj_inv, neg_mul, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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))⁻¹
neg₂ : ∀ (hx : ¬x = 0), ¬x.arg = π → (cexp (log x * n))⁻¹ = (cexp (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))⁻¹

Tactic:
split_ifs with hx hn ha ha
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : x = 0
hn : n = 0
ha : x.arg = π
⊢ Eq (α := ℂ) 1 1

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : x = 0
hn : n = 0
ha : ¬x.arg = π
⊢ Eq (α := ℂ) 1 1

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : x.arg = π
⊢ Eq (α := ℂ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : x = 0
hn : ¬n = 0
ha : ¬x.arg = π
⊢ Eq (α := ℂ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : ¬x = 0
h : x.arg = π
⊢ (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹ =
    (cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n))⁻¹

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : ¬x = 0
h : ¬x.arg = π
⊢ (cexp (log x * n))⁻¹ = (cexp (log x * n))⁻¹

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : x.arg ≠ π
rw :
  (if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))⁻¹
    else (x ^ n)⁻¹) =
    (x ^ n)⁻¹
rw₁ rw₂ : (x ^ n)⁻¹ = (x ^ n)⁻¹
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
rw [inv_cpow_eq_ite, if_neg hx]

Premises used: Complex.inv_cpow_eq_ite, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
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
⊢ (x ^ n)⁻¹ =
    if x.arg = π then (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x⁻¹ ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ))
    else x⁻¹ ^ n

Tactic:
rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]

Premises used: apply_ite, Complex.inv_cpow_eq_ite, Complex.conj_conj, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
pos : ∀ (h : x.arg = π), (x ^ n)⁻¹ = (x ^ n)⁻¹
neg : ∀ (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

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
h : x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
h : ¬x.arg = π
neg neg₁ : (x ^ n)⁻¹ = (x ^ n)⁻¹
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n

Tactic:
rw [inv_cpow _ _ h]

Premises used: Complex.inv_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
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)
⊢ HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n =
    if x.arg = π then x ^ n
    else (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) 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]

Premises used: Complex.log_conj_eq_ite, apply_ite, map_zero, map_eq_zero, map_mul, map_one, Complex.exp_conj, Complex.conj_conj, Complex.cpow_def, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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)
neg₂ :
  ∀ (hcx : ¬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 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:
split_ifs with hcx hn hx
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hcx : x = 0
hn : n = 0
hx : x.arg = π
⊢ Eq (α := ℂ) 1 1

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hcx : x = 0
hn : n = 0
hx : ¬x.arg = π
⊢ Eq (α := ℂ) 1 1

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h : x.arg = π
⊢ Eq (α := ℂ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hcx : x = 0
hn : ¬n = 0
h : ¬x.arg = π
⊢ Eq (α := ℂ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hcx : ¬x = 0
h : x.arg = π
⊢ cexp (log x * n) = cexp (log x * n)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hcx : ¬x = 0
h : ¬x.arg = π
⊢ cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n) =
    cexp (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) n)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
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 : ℂ))
rw₁ rw₂ :
  Eq (α := ℂ) ((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 : ℂ))

Tactic:
rw [conj_cpow_eq_ite, if_neg hx]

Premises used: Complex.conj_cpow_eq_ite, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
x n : ℂ
hx : x.arg ≠ π
rw :
  HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)) : ℂ)
rw₁ rw₂ :
  HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
    HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ)
⊢ HPow.hPow (β := ℂ) x ((starRingEnd ℂ : (a : ℂ) → ℂ) n : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) n)

Tactic:
rw [conj_cpow _ _ hx, conj_conj]

Premises used: Complex.conj_cpow, Complex.conj_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℕ
z : ℂ
H : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = 0 ∧ z ≠ 0
⊢ False ∧ ¬z = 0

Tactic:
norm_cast at H
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False

Tactic:
H.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex
Goal:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False

Tactic:
exact H.1

Premises used: And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
rw : Eq (α := ℂ) 0 (0 x)
rw₁ rw₂ : Eq (α := ℂ) 0 0
⊢ HPow.hPow (α := ℂ) 0 x = 0 x

Tactic:
rw [zero_cpow hx, Pi.zero_apply]

Premises used: Pi.zero_apply, Complex.zero_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
b : ℂ
hb : b ≠ 0
suffices : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
⊢ (𝓝 b).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ HPow.hPow (α := ℂ) 0 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0

Tactic:
IsOpen.eventually_mem isOpen_ne hb

Premises used: Set.Mem, IsOpen.eventually_mem, isOpen_ne, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0

Tactic:
exact IsOpen.eventually_mem isOpen_ne hb

Premises used: IsOpen.eventually_mem, isOpen_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
x : ℂ
hx : x ≠ 0
rw rw₁ : cexp (Complex.log x * b) = cexp (Complex.log x * b)
⊢ x ^ b = cexp (Complex.log x * b)

Tactic:
rw [cpow_def_of_ne_zero hx]

Premises used: Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
suffices : ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0
⊢ (𝓝 a).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ x ^ b) fun (x : ℂ) ↦ cexp (Complex.log x * b)

Tactic:
suffices ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [cpow_def_of_ne_zero hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0

Tactic:
IsOpen.eventually_mem isOpen_ne ha

Premises used: Set.Mem, IsOpen.eventually_mem, isOpen_ne, Not
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 a, x ≠ 0

Tactic:
exact IsOpen.eventually_mem isOpen_ne ha

Premises used: IsOpen.eventually_mem, isOpen_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
this : IsOpen (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}ᶜ
x : ℂ × ℂ
hx : Membership.mem (γ := Set (ℂ × ℂ)) {x : ℂ × ℂ | x.1 = 0}ᶜ x
⊢ Membership.mem (γ := Set (ℂ × ℂ))
    {x : ℂ × ℂ |
      (fun (x : ℂ × ℂ) ↦
          Eq (α := ℂ) ((fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) x) ((fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)) x))
        x}
    x

Tactic:
simp_all [cpow_def_of_ne_zero]

Premises used: Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
suffices : IsOpen (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}ᶜ
⊢ (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)

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⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
rw : IsClosed (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}
⊢ IsOpen (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}ᶜ

Tactic:
rw [isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsClosed (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}

Tactic:
isClosed_eq continuous_fst continuous_const

Premises used: continuous_const, continuous_fst, isClosed_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ≠ 0
⊢ IsClosed (X := ℂ × ℂ) {x : ℂ × ℂ | x.1 = 0}

Tactic:
exact isClosed_eq continuous_fst continuous_const

Premises used: continuous_const, continuous_fst, isClosed_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
h : ∀ (b : ℂ), a ^ b = cexp (Complex.log a * b)
⊢ Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ a ^ x) fun (x : ℂ) ↦ cexp (Complex.log a * x)

Tactic:
ext1 b
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b_1 : ℂ
ha : a ≠ 0
b : ℂ
h h₁ : cexp (Complex.log a * b) = cexp (Complex.log a * b)
⊢ a ^ b = cexp (Complex.log a * b)

Tactic:
rw [cpow_def_of_ne_zero ha]

Premises used: Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ≠ 0
cpow_eq : Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ a ^ x) fun (x : ℂ) ↦ cexp (Complex.log a * x)
rw : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ cexp (Complex.log a * x)) b
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b

Tactic:
rw [cpow_eq]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
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 : ℂ) ↦ cexp (Complex.log a * x)) b

Tactic:
continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)

Premises used: Complex.continuous_exp, continuousAt_const, Continuous.continuousAt, ContinuousAt.mul, ContinuousAt.comp, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
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 : ℂ) ↦ cexp (Complex.log a * x)) b

Tactic:
exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
h : b ≠ 0
pos : ∀ (ha : a = 0), ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
neg : ∀ (ha : ¬a = 0), ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
h : b ≠ 0
ha : a = 0
pos : ContinuousAt (Y := ℂ) 0 b
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b

Tactic:
rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]

Premises used: continuousAt_congr, zero_cpow_eq_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (Y := ℂ) 0 b

Tactic:
continuousAt_const

Premises used: continuousAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (Y := ℂ) 0 b

Tactic:
exact continuousAt_const

Premises used: continuousAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b

Tactic:
continuousAt_const_cpow ha

Premises used: continuousAt_const_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ a ^ x) b

Tactic:
exact continuousAt_const_cpow ha

Premises used: continuousAt_const_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
rw : ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)) p
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) p

Tactic:
rw [continuousAt_congr (cpow_eq_nhds' <| slitPlane_ne_zero hp_fst)]

Premises used: continuousAt_congr, cpow_eq_nhds', Complex.slitPlane_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)) p

Tactic:
continuous_exp.continuousAt.comp ?_

Premises used: Complex.continuous_exp, Continuous.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
refine : ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ Complex.log x.1 * x.2) p
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ cexp (Complex.log x.1 * x.2)) p

Tactic:
refine continuous_exp.continuousAt.comp ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ Complex.log x.1 * x.2) p

Tactic:
ContinuousAt.mul
      (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
      continuous_snd.continuousAt

Premises used: continuous_snd, continuous_fst, continuousAt_clog, Continuous.continuousAt, ContinuousAt.mul, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
p : ℂ × ℂ
hp_fst : p.1 ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ Complex.log x.1 * x.2) p

Tactic:
exact
    ContinuousAt.mul
      (ContinuousAt.comp (continuousAt_clog hp_fst) continuous_fst.continuousAt)
      continuous_snd.continuousAt

Premises used: continuous_snd, continuous_fst, continuousAt_clog, Continuous.continuousAt, ContinuousAt.mul, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
a b : ℂ
ha : a ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ b) a

Tactic:
Tendsto.comp (@continuousAt_cpow (a, b) ha) (continuousAt_id.prodMk continuousAt_const)

Premises used: ContinuousAt, continuousAt_cpow, continuousAt_const, Filter.Tendsto.comp, ContinuousAt.prodMk, continuousAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f g : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
ha : a ∈ slitPlane
⊢ Tendsto (fun (x : α) ↦ f x ^ g x) l (𝓝 (a ^ b))

Tactic:
(@continuousAt_cpow (a, b) ha).tendsto.comp (hf.prodMk_nhds hg)

Premises used: continuousAt_cpow, ContinuousAt.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))

Tactic:
(continuousAt_const_cpow h).tendsto.comp hf

Premises used: continuousAt_const_cpow, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0
⊢ Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))

Tactic:
exact (continuousAt_const_cpow h).tendsto.comp hf

Premises used: continuousAt_const_cpow, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))

Tactic:
(continuousAt_const_cpow' h).tendsto.comp hf

Premises used: continuousAt_const_cpow', ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : b ≠ 0
⊢ Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))

Tactic:
exact (continuousAt_const_cpow' h).tendsto.comp hf

Premises used: continuousAt_const_cpow', ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
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))
inr : ∀ (h : b ≠ 0), Tendsto (fun (x : α) ↦ a ^ f x) l (𝓝 (a ^ b))
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℂ
s : Set α
a : α
hf : ContinuousWithinAt f s a
hg : ContinuousWithinAt g s a
h0 : f a ∈ slitPlane
⊢ ContinuousWithinAt (Y := ℂ) (fun (x : α) ↦ f x ^ g x) s a

Tactic:
hf.cpow hg h0

Premises used: ContinuousWithinAt, Filter.Tendsto.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
a : α
b : ℂ
hf : ContinuousWithinAt f s a
h : b ≠ 0 ∨ f a ≠ 0
⊢ ContinuousWithinAt (Y := ℂ) (fun (x : α) ↦ b ^ f x) s a

Tactic:
hf.const_cpow h

Premises used: ContinuousWithinAt, Filter.Tendsto.const_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℂ
a : α
hf : ContinuousAt f a
hg : ContinuousAt g a
h0 : f a ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : α) ↦ f x ^ g x) a

Tactic:
hf.cpow hg h0

Premises used: ContinuousAt, Filter.Tendsto.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
a : α
b : ℂ
hf : ContinuousAt f a
h : b ≠ 0 ∨ f a ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : α) ↦ b ^ f x) a

Tactic:
hf.const_cpow h

Premises used: ContinuousAt, Filter.Tendsto.const_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f g : α → ℂ
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
h0 : ∀ a ∈ s, f a ∈ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (x : α) ↦ f x ^ g x) s

Tactic:
fun a ha =>
  (hf a ha).cpow (hg a ha) (h0 a ha)

Premises used: ContinuousWithinAt.cpow, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
b : ℂ
hf : ContinuousOn f s
h : b ≠ 0 ∨ ∀ a ∈ s, f a ≠ 0
⊢ ContinuousOn (Y := ℂ) (fun (x : α) ↦ b ^ f x) s

Tactic:
fun a ha => (hf a ha).const_cpow (h.imp id fun h => h a ha)

Premises used: id, ContinuousOn, Or.imp, ContinuousWithinAt.const_cpow