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

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

case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) :=
  continuous_ofReal.continuousAt.prod_map continuousAt_id
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ 0 < (↑(x, y).fst, (x, y).snd).fst.re
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
refine' (continuousAt_cpow (Or.inl _)).comp this
no goals
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p => (↑p.fst, p.snd)) (x, y)
⊢ 0 < (↑(x, y).fst, (x, y).snd).fst.re
rwa [ofReal_re]
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ := by
  rw [ofReal_zero]
  apply continuousAt_cpow_zero_of_re_pos
  tauto
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
B : ContinuousAt (fun p => (↑p.fst, p.snd)) (0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ :=
  continuous_ofReal.continuousAt.prod_map continuousAt_id
no goals
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
A : ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
B : ContinuousAt (fun p => (↑p.fst, p.snd)) (0, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (0, y)
exact @ContinuousAt.comp (ℝ × ℂ) (ℂ × ℂ) ℂ _ _ _ _ (fun p => ⟨↑p.1, p.2⟩) ⟨0, y⟩ A B
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (↑0, y)
rw [ofReal_zero]
case hz
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p => p.fst ^ p.snd) (0, y)
apply continuousAt_cpow_zero_of_re_pos
no goals
case hz
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ 0 < y.re
tauto
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
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
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) :=
  ContinuousAt.prod_map continuous_ofReal.continuousAt.neg continuousAt_id
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => (-↑x.fst) ^ x.snd) (x, y)

case inr.inr.hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => exp (↑π * I * x.snd)) (x, y)
case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
apply ContinuousAt.mul
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ∀ (x : ℝ × ℂ),
    x ∈ Set.Iio 0 ×ˢ Set.univ → (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) x = (fun p => ↑p.fst ^ p.snd) x
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ContinuousAt (fun p => ↑p.fst ^ p.snd) (x, y)
refine' this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) _)
no goals
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) (x, y)
⊢ ∀ (x : ℝ × ℂ),
    x ∈ Set.Iio 0 ×ˢ Set.univ → (fun p => (-↑p.fst) ^ p.snd * exp (↑π * I * p.snd)) x = (fun p => ↑p.fst ^ p.snd) x
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ 0 < (-↑(x, y).fst, (x, y).snd).fst.re
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => (-↑x.fst) ^ x.snd) (x, y)
refine' (continuousAt_cpow (Or.inl _)).comp A
no goals
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ 0 < (-↑(x, y).fst, (x, y).snd).fst.re
rwa [neg_re, ofReal_re, neg_pos]
no goals
case inr.inr.hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p => (-↑p.fst, p.snd)) (x, y)
⊢ ContinuousAt (fun x => exp (↑π * I * x.snd)) (x, y)
exact (continuous_exp.comp (continuous_const.mul continuous_snd)).continuousAt