-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
    ContinuousAt (fun p => (p.1 : ℂ) ^ p.2 : ℝ × ℂ → ℂ) (x, y)

Proof state:
case inr.inr.hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun x => cexp (↑π * I * x.2)) (x, y)

Tactic:
exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt

Result:
no goals

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Tactic:
refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)

Result:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)
⊢ ∀ x ∈ Set.Iio 0 ×ˢ Set.univ, (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) x = (fun p => ↑p.1 ^ p.2) x

Proof state:
case hz
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re

Tactic:
tauto

Result:
no goals

Proof state:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)

Tactic:
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop

Result:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)

Proof state:
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.1 ^ p.2) (↑0, y)
⊢ ContinuousAt (fun p => (↑p.1, p.2)) (0, y)

Tactic:
fun_prop

Result:
no goals

Proof state:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Tactic:
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop

Result:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Proof state:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Tactic:
suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
  refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
  exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm

Result:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)

Proof state:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ 0 < (-↑(x, y).1, (x, y).2).1.re

Tactic:
rwa [neg_re, ofReal_re, neg_pos]

Result:
no goals

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p => (↑p.1, p.2)) (x, y)

Tactic:
fun_prop

Result:
no goals

Proof state:
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Tactic:
apply continuousAt_cpow_zero_of_re_pos

Result:
case hz
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re

Proof state:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.1, p.2)) (x, y)
⊢ 0 < (↑(x, y).1, (x, y).2).1.re

Tactic:
rwa [ofReal_re]

Result:
no goals

Proof state:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun x => (-↑x.1) ^ x.2) (x, y)

Tactic:
refine (continuousAt_cpow (Or.inl ?_)).comp A

Result:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ 0 < (-↑(x, y).1, (x, y).2).1.re

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Tactic:
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)

Result:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)

case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Proof state:
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)

Tactic:
apply ContinuousAt.mul

Result:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun x => (-↑x.1) ^ x.2) (x, y)

case inr.inr.hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun x => cexp (↑π * I * x.2)) (x, y)

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.1, p.2)) (x, y)

Tactic:
fun_prop

Result:
no goals

Proof state:
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) (↑0, y)

Tactic:
rw [ofReal_zero]

Result:
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.1 ^ p.2) (0, y)

Proof state:
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.1 ^ p.2) (↑0, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)

Tactic:
have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop

Result:
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.1 ^ p.2) (↑0, y)
B : ContinuousAt (fun p => (↑p.1, p.2)) (0, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)

Proof state:
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.1 ^ p.2) (↑0, y)
B : ContinuousAt (fun p => (↑p.1, p.2)) (0, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)

Tactic:
exact A.comp_of_eq B rfl

Result:
no goals

Proof state:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)
⊢ ∀ x ∈ Set.Iio 0 ×ˢ Set.univ, (fun p => (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) x = (fun p => ↑p.1 ^ p.2) x

Tactic:
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm

Result:
no goals

Proof state:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (x, y)

Tactic:
refine (continuousAt_cpow (Or.inl ?_)).comp this

Result:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.1, p.2)) (x, y)
⊢ 0 < (↑(x, y).1, (x, y).2).1.re

Proof state:
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)

Tactic:
have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ := by
  rw [ofReal_zero]
  apply continuousAt_cpow_zero_of_re_pos
  tauto

Result:
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.1 ^ p.2) (↑0, y)
⊢ ContinuousAt (fun p => ↑p.1 ^ p.2) (0, y)