awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2)
have rw : rexp (log x.1 * x.2) = rexp (log x.1 * x.2)
Tactic: rw [rpow_def_of_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp_fst : 0 < p.1
⊢ (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
have suffices : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
Tactic: suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, 0 < x.1 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [rpow_def_of_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have hp₁ : p.1 < 0 ∨ 0 < p.1
Tactic: rw [ne_iff_lt_or_gt] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have inl : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) p
Tactic: rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) p
have inl : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p
Tactic: refine ContinuousAt.mul ?_ (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p
have inl : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p
Tactic: refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have inr : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p
Tactic: rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)) p
have inr : ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p
Tactic: refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ × ℝ) ↦ log x.1) p
have inr : p.1 ≠ 0
Tactic: refine (continuousAt_log ?_).comp continuous_fst.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0 ∨ 0 < p.1
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have inl : ∀ (hp : p.1 < 0), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
Tactic: cases hp with
  | inl hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt
  | inr hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : p.1 < 0 ∨ 0 < p.1
inl : ∀ (hp : p.1 < 0), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have inr : ∀ (hp : 0 < p.1), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
Tactic: cases hp with
  | inl hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_neg hp)]
    refine ContinuousAt.mul ?_ (by fun_prop)
    · refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
      exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt
  | inr hp =>
    rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℝ × ℝ
hp : 0 < p.2
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
have obtain : ∀ (x y : ℝ) (hp : 0 < (x, y).2), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
Tactic: obtain ⟨x, y⟩ := p
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
have inl : ∀ (hx : x ≠ 0), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
Tactic: obtain hx | rfl := ne_or_eq x 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ
hp : 0 < y
inl : ∀ (hx : x ≠ 0), ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (x, y)
have inr : ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (0, y)
Tactic: obtain hx | rfl := ne_or_eq x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
y : ℝ
hp : 0 < y
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (0, y)
have A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
Tactic: have A : Tendsto (fun p : ℝ × ℝ => exp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
    tendsto_exp_atBot.comp
      ((tendsto_log_nhdsNE_zero.comp tendsto_fst).atBot_mul_pos hp tendsto_snd)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (0, y)
have B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
Tactic: have B : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
    squeeze_zero_norm (fun p => abs_rpow_le_exp_log_mul p.1 p.2) A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[{0}] 0) (𝓝 y)) (pure 0)
have rw : ∀ᶠ (a : ℝ) in 𝓝 y, HPow.hPow (α := ℝ) (0, a).1 (0, a).2 = 0
Tactic: rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
y : ℝ
hp : 0 < y
A : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ rexp (log p.1 * p.2)) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
B : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[≠] 0) (𝓝 y)) (𝓝 0)
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (0, y)
have C : Tendsto (β := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) (SProd.sprod (α := Filter ℝ) (𝓝[{0}] 0) (𝓝 y)) (pure 0)
Tactic: have C : Tendsto (fun p : ℝ × ℝ => p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0) := by
    rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]
    exact (lt_mem_nhds hp).mono fun y hy => zero_rpow hy.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
x q : ℝ
h : x ≠ 0 ∨ 0 ≤ q
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x
have h₁ : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
Tactic: rw [le_iff_lt_or_eq, ← or_assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x q : ℝ
h : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x
have inl : ∀ (h : x ≠ 0 ∨ 0 < q), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x
Tactic: obtain h | rfl := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x q : ℝ
h : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
inl : ∀ (h : x ≠ 0 ∨ 0 < q), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ q) x
have inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) x
Tactic: obtain h | rfl := h
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) x
have inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1) x
Tactic: simp_rw [rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
z : ℂ
hz : 0 < z.re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (0, z)
have hz₀ : z ≠ 0
Tactic: have hz₀ : z ≠ 0 := ne_of_apply_ne re hz.ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (0, z)
have rw : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)
Tactic: rw [ContinuousAt, zero_cpow hz₀, tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1 ^ x.2‖) (𝓝 (0, z)) (𝓝 0)
have refine : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)
Tactic: refine squeeze_zero (fun _ => norm_nonneg _) (fun _ => norm_cpow_le _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re / rexp (x.1.arg * x.2.im)) (𝓝 (0, z)) (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)
Tactic: simp only [div_eq_mul_inv, ← Real.exp_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)
have refine_1 : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)
Tactic: refine Tendsto.zero_mul_isBoundedUnder_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
refine_1 : Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re * rexp (-(x.1.arg * x.2.im))) (𝓝 (0, z)) (𝓝 0)
have refine_2 : IsBoundedUnder (β := ℂ × ℂ) (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z))
  ((fun (x : ℝ) ↦ ‖x‖) ∘ fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im)))
Tactic: refine Tendsto.zero_mul_isBoundedUnder_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)
have h : 0 = Norm.norm (E := ℂ) (0, z).1 ^ Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)
Tactic: convert!
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
h : 0 = Norm.norm (E := ℂ) (0, z).1 ^ Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)
⊢ Tendsto (β := ℝ) (fun (x : ℂ × ℂ) ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)
have refine_1 : Norm.norm (E := ℂ) (0, z).1 ≠ 0 ∨ 0 < Function.comp (α := ℂ × ℂ) re Prod.snd (0, z)
Tactic: convert!
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (β := ℂ × ℂ) (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z))
    ((fun (x : ℝ) ↦ ‖x‖) ∘ fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im)))
have refine_2 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))
Tactic: simp only [Function.comp_def, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))
have refine_2 : ∀ (C : ℝ) (hC : |z.im| < C),
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))
Tactic: rcases exists_gt |im z| with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 (0, z)) fun (x : ℂ × ℂ) ↦ rexp (-(x.1.arg * x.2.im))
have refine_2 : ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (rexp (-(a.1.arg * a.2.im))) (rexp (π * C))
Tactic: refine ⟨Real.exp (π * C), eventually_map.2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
C : ℝ
hC : |z.im| < C
⊢ ∀ᶠ (a : ℂ × ℂ) in 𝓝 (0, z), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (rexp (-(a.1.arg * a.2.im))) (rexp (π * C))
have refine_2 : ∀ (z : ℂ × ℂ) (hz : |(im ∘ Prod.snd) z| < C), |z.1.arg * z.2.im| ≤ π * C
Tactic: refine
      (((continuous_im.comp continuous_snd).abs.tendsto (_, z)).eventually (gt_mem_nhds hC)).mono
        fun z hz => Real.exp_le_exp.2 <| (neg_le_abs _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z_1 : ℂ
hz_1 : 0 < z_1.re
hz₀ : z_1 ≠ 0
C : ℝ
hC : |z_1.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg * z.2.im| ≤ π * C
have refine_2 : |z.1.arg| * |z.2.im| ≤ π * C
Tactic: rw [_root_.abs_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
p : ℂ × ℂ
h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0
h₂ : 0 < p.2.re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) p
have obtain : ∀ (z w : ℂ) (h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0) (h₂ : 0 < (z, w).2.re),
  ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
Tactic: obtain ⟨z, w⟩ := p
Cleared hypotheses: p, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
z w : ℂ
h₁ : 0 ≤ (z, w).1.re ∨ (z, w).1.im ≠ 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
have h₃ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
Tactic: rw [← not_lt_zero_iff, lt_iff_le_and_ne, not_and_or, Ne, Classical.not_not,
    not_le_zero_iff] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
have inl : ∀ (h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0), ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
Tactic: rcases h₁ with (h₁ | (rfl : z = 0))
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
z w : ℂ
h₁ : (0 < (z, w).1.re ∨ (z, w).1.im ≠ 0) ∨ (z, w).1 = 0
h₂ : 0 < (z, w).2.re
inl : ∀ (h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0), ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (z, w)
have inr : ∀ (h₂ : 0 < (0, w).2.re), ContinuousAt (Y := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) (0, w)
Tactic: rcases h₁ with (h₁ | (rfl : z = 0))
Cleared hypotheses: z, h₁, h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have inl : ∀ (hx : 0 < x), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
Tactic: rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
inl : ∀ (hx : 0 < x), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have inr : ∀ (h : 0 < y.re ∨ Ne (α := ℝ) 0 0), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)
Tactic: rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
inl : ∀ (hx : 0 < x), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
inr : ∀ (h : 0 < y.re ∨ Ne (α := ℝ) 0 0), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have inr₁ : ∀ (hx : x < 0), ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
Tactic: rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have this : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)
Tactic: have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have inl : 0 < ((↑(x, y).1 : ℂ), (x, y).2).1.re
Tactic: refine (continuousAt_cpow (Or.inl ?_)).comp this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (x, y)
⊢ 0 < ((↑(x, y).1 : ℂ), (x, y).2).1.re
have inl : 0 < (x, y).1
Tactic: rwa [ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
⊢ ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) (0, y)
have hz : 0 < y.re
Tactic: apply continuousAt_cpow_zero_of_re_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
⊢ 0 < y.re
have hz : ∀ (h : 0 < y.re), 0 < y.re
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
hz : ∀ (h : 0 < y.re), 0 < y.re
⊢ 0 < y.re
have hz₁ : ∀ (h : Ne (α := ℝ) 0 0), 0 < y.re
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)
have A : ContinuousAt (Y := ℂ) (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
y : ℂ
h : 0 < y.re ∨ Ne (α := ℝ) 0 0
A : ContinuousAt (Y := ℂ) (fun (p : ℂ × ℂ) ↦ p.1 ^ p.2) ((↑0 : ℂ), y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (0, y)
have B : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ ((↑p.1 : ℂ), p.2)) (0, y)
Tactic: have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have refine : ∀ x ∈ SProd.sprod (α := Set ℝ) (β := Set ℂ) (Set.Iio 0) Set.univ,
  Eq (α := ℂ) ((fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) x)
    ((fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) x)
Tactic: refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (↑p.1 : ℂ) ^ p.2) (x, y)
have inr : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
have A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
Tactic: have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
have inr : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2) (x, y)
Tactic: apply ContinuousAt.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
inr : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2 * cexp ((↑π : ℂ) * I * p.2)) (x, y)
have inr₁ : ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ cexp ((↑π : ℂ) * I * p.2)) (x, y)
Tactic: apply ContinuousAt.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
⊢ ContinuousAt (Y := ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ)) ^ p.2) (x, y)
have inr : 0 < (-(↑(x, y).1 : ℂ), (x, y).2).1.re
Tactic: refine (continuousAt_cpow (Or.inl ?_)).comp A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
⊢ 0 < (-(↑(x, y).1 : ℂ), (x, y).2).1.re
have inr : 0 < -(↑(x, y).1 : ℂ).re
Tactic: rwa [neg_re, ofReal_re, neg_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
inr : 0 < -(↑(x, y).1 : ℂ).re
⊢ 0 < (-(↑(x, y).1 : ℂ), (x, y).2).1.re
have inr₁ : 0 < -(x, y).1
Tactic: rwa [neg_re, ofReal_re, neg_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (Y := ℂ × ℂ) (fun (p : ℝ × ℂ) ↦ (-(↑p.1 : ℂ), p.2)) (x, y)
inr : 0 < -(↑(x, y).1 : ℂ).re
inr₁ : 0 < -(x, y).1
⊢ 0 < (-(↑(x, y).1 : ℂ), (x, y).2).1.re
have inr₂ : (x, y).1 < 0
Tactic: rwa [neg_re, ofReal_re, neg_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ Eq (α := (p : ℝ≥0 × ℝ) → ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2)
    (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2))
have h₁ : ∀ (p : ℝ≥0 × ℝ),
  (↑(p.1 ^ p.2) : ℝ) = (↑((toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) p) : ℝ)
Tactic: ext p