awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
p : ℝ≥0 × ℝ
⊢ (↑(p.1 ^ p.2) : ℝ) = (↑((toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) p) : ℝ)
have h₁ : 0 ≤ (↑p.1 : ℝ) ^ p.2
Tactic: simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
⊢ ContinuousAt (Y := ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2) (x, y)
have this : 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))
Tactic: have :
    (fun p : ℝ≥0 × ℝ => p.1 ^ p.2) =
      Real.toNNReal ∘ (fun p : ℝ × ℝ => p.1 ^ p.2) ∘ fun p : ℝ≥0 × ℝ => (p.1.1, p.2) := by
    ext p
    simp only [coe_rpow, val_eq_coe, Function.comp_apply, coe_toNNReal', left_eq_sup]
    positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  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))
⊢ ContinuousAt (Y := ℝ≥0) (fun (p : ℝ≥0 × ℝ) ↦ p.1 ^ p.2) (x, y)
have rw : ContinuousAt (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  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))
⊢ ContinuousAt (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)
have refine_1 : ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ((↑(x, y).1 : ℝ), (x, y).2)
Tactic: refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  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))
refine_1 : ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ((↑(x, y).1 : ℝ), (x, y).2)
⊢ ContinuousAt (toNNReal ∘ (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ∘ fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)
have refine_2 : ContinuousAt (Y := ℝ × ℝ) (fun (p : ℝ≥0 × ℝ) ↦ ((↑p.1 : ℝ), p.2)) (x, y)
Tactic: refine continuous_real_toNNReal.continuousAt.comp (ContinuousAt.comp ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this :
  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))
⊢ ContinuousAt (Y := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) ((↑(x, y).1 : ℝ), (x, y).2)
have refine_1 : ((↑(x, y).1 : ℝ), (x, y).2).1 ≠ 0 ∨ 0 < ((↑(x, y).1 : ℝ), (x, y).2).2
Tactic: apply Real.continuousAt_rpow
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ≥0
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have obtain : ∀ (m : ℕ) (hm : x < (y - 1 + 1) ^ m), ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have hm₁ : x < y ^ m
Tactic: rw [tsub_add_cancel_of_le hy.le] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have refine : ∀ (n : ℕ) (hn : n ≥ m + 1), x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: refine eventually_atTop.2 ⟨m + 1, fun n hn => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have simp : HPow.hPow (β := ℝ) x (↑n : ℝ)⁻¹ ≤ y
Tactic: simp only [one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
hx : x ≠ ∞
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have lift : ∀ (x : ℝ≥0), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: lift x to ℝ≥0 using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have pos : ∀ (h : y = ∞), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: by_cases h : y = ∞
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
pos : ∀ (h : y = ∞), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have neg : ∀ (h : ¬y = ∞), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: by_cases h : y = ∞
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
h : ¬y = ∞
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
have neg : ∀ (y : ℝ≥0) (hy : 1 < (↑y : ℝ≥0∞)), ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
Tactic: lift y to ℝ≥0 using h
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
have this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: have := NNReal.eventually_pow_one_div_le x (mod_cast hy : 1 < y)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
⊢ ∀ᶠ (n : ℕ) in atTop, (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
have neg : ∀ (n : ℕ), x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
Tactic: refine this.congr (Eventually.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
n : ℕ
⊢ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
have neg : x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑(x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ≤ (↑y : ℝ≥0∞)
Tactic: rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x y : ℝ≥0
hy : 1 < (↑y : ℝ≥0∞)
this : ∀ᶠ (n : ℕ) in atTop, x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
n : ℕ
neg : x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑(x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) : ℝ≥0∞) ≤ (↑y : ℝ≥0∞)
⊢ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ (↑x : ℝ≥0∞) ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑y : ℝ≥0∞)
have neg₁ : x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y ↔ x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ y
Tactic: rw [← coe_rpow_of_nonneg x (by positivity : 0 ≤ (1 / n : ℝ)), coe_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have pos : ∀ (hx : x = ∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
Tactic: by_cases hx : x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
pos : ∀ (hx : x = ∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have neg : ∀ (hx : ¬x = ∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
Tactic: by_cases hx : x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have pos : Tendsto (fun (a : ℝ≥0∞) ↦ a ^ y) (𝓝 ∞) (𝓝 (HPow.hPow (α := ℝ≥0∞) ∞ y))
Tactic: rw [hx, ContinuousAt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ∞
⊢ Tendsto (fun (a : ℝ≥0∞) ↦ a ^ y) (𝓝 ∞) (𝓝 (HPow.hPow (α := ℝ≥0∞) ∞ y))
have h₁ : HPow.hPow (α := ℝ≥0∞) ∞ y = ∞
Tactic: convert! ENNReal.tendsto_rpow_at_top h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have neg : ∀ (x : ℝ≥0), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) (↑x : ℝ≥0∞)
Tactic: lift x to ℝ≥0 using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) (↑x : ℝ≥0∞)
have neg : ContinuousAt (Y := ℝ≥0∞) ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x
Tactic: rw [continuousAt_coe_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (Y := ℝ≥0∞) ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x
have h₁ : (fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal = ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y
Tactic: convert! continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal = ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y
have h₁ : ∀ (x : ℝ≥0), ((fun (a : ℝ≥0∞) ↦ a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun (z : ℝ≥0) ↦ z ^ y) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
⊢ Continuous (Y := ℝ≥0∞) fun (a : ℝ≥0∞) ↦ a ^ y
have refine : ∀ (x : ℝ≥0∞), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
Tactic: refine continuous_iff_continuousAt.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have inl : ∀ (hy : 0 < y), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
Tactic: rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
x : ℝ≥0∞
inl : ∀ (hy : 0 < y), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℝ) a 0) x
Tactic: rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
x : ℝ≥0∞
inl : ∀ (hy : 0 < y), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℝ) a 0) x
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have inr₁ : ∀ (hy : y < 0), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
Tactic: rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
x : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ HPow.hPow (β := ℝ) a 0) x
have inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ 1) x
Tactic: simp only [rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have inr : ∀ (z : ℝ) (hz : y = -z), ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
Tactic: obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (hypothesis)
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have z_pos : 0 < z
Tactic: have z_pos : 0 < z := by simpa [hz] using hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ a ^ y) x
have inr : ContinuousAt (Y := ℝ≥0∞) (fun (a : ℝ≥0∞) ↦ (a ^ z)⁻¹) x
Tactic: simp_rw [hz, rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
⊢ Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ c * x ^ y) (𝓝 0) (𝓝 0)
have h : 0 = c * HPow.hPow (α := ℝ≥0∞) 0 y
Tactic: convert! ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Continuity (goal)
Goal:
c : ℝ≥0∞
hc : c ≠ ∞
y : ℝ
hy : 0 < y
h : 0 = c * HPow.hPow (α := ℝ≥0∞) 0 y
⊢ Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ c * x ^ y) (𝓝 0) (𝓝 0)
have convert_3 : HPow.hPow (α := ℝ≥0∞) 0 y ≠ 0 ∨ c ≠ ∞
Tactic: convert! ENNReal.Tendsto.const_mul (ENNReal.continuous_rpow_const.tendsto 0) _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p
have A : p.1 ≠ 0
Tactic: have A : p.1 ≠ 0 := slitPlane_ne_zero hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p
have this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
Tactic: have : (fun x : ℂ × ℂ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
    ((isOpen_ne.preimage continuous_fst).eventually_mem A).mono fun p hp =>
      cpow_def_of_ne_zero hp _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p
have rw : HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
  (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
    p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
  p
Tactic: rw [cpow_sub _ _ A, cpow_one, mul_div_left_comm, mul_smul, mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
A : p.1 ≠ 0
this : (𝓝 p).EventuallyEq (β := ℂ) (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p
have refine : HasStrictFDerivAt (fun (x : ℂ × ℂ) ↦ cexp (log x.1 * x.2))
  (p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 / p.1) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
    p.1 ^ p.2 • HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
  p
Tactic: refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ x ^ y) (x ^ y * log x) y
have inl : ∀ (h : Ne (α := ℂ) 0 0 ∨ y ≠ 0),
  HasStrictDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) (HPow.hPow (α := ℂ) 0 y * log 0) y
Tactic: rcases em (x = 0) with (rfl | hx)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
inl :
  ∀ (h : Ne (α := ℂ) 0 0 ∨ y ≠ 0),
    HasStrictDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) (HPow.hPow (α := ℂ) 0 y * log 0) y
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ x ^ y) (x ^ y * log x) y
have inr : ∀ (hx : ¬x = 0), HasStrictDerivAt (fun (y : ℂ) ↦ x ^ y) (x ^ y * log x) y
Tactic: rcases em (x = 0) with (rfl | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
y : ℂ
h : Ne (α := ℂ) 0 0 ∨ y ≠ 0
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) (HPow.hPow (α := ℂ) 0 y * log 0) y
have h₁ : y ≠ 0
Tactic: replace h := h.neg_resolve_left rfl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) (HPow.hPow (α := ℂ) 0 y * log 0) y
have inl : HasStrictDerivAt (F := ℂ) (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) 0 y
Tactic: rw [log_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
y : ℂ
h : y ≠ 0
⊢ HasStrictDerivAt (F := ℂ) (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y) 0 y
have inl : (𝓝 y).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ 0) fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y
Tactic: refine (hasStrictDerivAt_const y 0).congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have pos : ∀ (h : UniqueDiffWithinAt ℂ s x), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Tactic: by_cases h : UniqueDiffWithinAt ℂ s x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
pos : ∀ (h : UniqueDiffWithinAt ℂ s x), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg : ∀ (h : ¬UniqueDiffWithinAt ℂ s x), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Tactic: by_cases h : UniqueDiffWithinAt ℂ s x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg : 0 = log c * derivWithin f s x * c ^ f x
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt h,
      derivWithin_zero_of_not_uniqueDiffWithinAt h, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
neg : 0 = log c * derivWithin f s x * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg₁ : 0 = log c * 0 * c ^ f x
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt h,
      derivWithin_zero_of_not_uniqueDiffWithinAt h, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
neg : 0 = log c * derivWithin f s x * c ^ f x
neg₁ : 0 = log c * 0 * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg₂ : 0 = 0 * c ^ f x
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt h,
      derivWithin_zero_of_not_uniqueDiffWithinAt h, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
neg : 0 = log c * derivWithin f s x * c ^ f x
neg₁ : 0 = log c * 0 * c ^ f x
neg₂ : 0 = 0 * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg₃ : Eq (α := ℂ) 0 0
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt h,
      derivWithin_zero_of_not_uniqueDiffWithinAt h, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have pos : ∀ (hc : c = 0), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
pos : ∀ (hc : c = 0), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg : ∀ (hc : ¬c = 0), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have neg : derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = c ^ f x * log c * derivWithin f s x
Tactic: rw [mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : c = 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have h₁ : (𝓝[s \ {x}] x).NeBot
Tactic: rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin] at h
Cleared hypotheses: h, hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
have pos : Eq (α := ℂ) (derivWithin (fun (x : ℂ) ↦ HPow.hPow (α := ℂ) 0 (f x)) s x) 0
Tactic: simp only [hc, log_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ Eq (α := ℂ) (derivWithin (fun (x : ℂ) ↦ HPow.hPow (α := ℂ) 0 (f x)) s x) 0
have pos : ∃ᶠ (y : ℂ) in 𝓝[s \ {x}] x, Membership.mem (γ := Set ℂ) {0, 1} (HPow.hPow (α := ℂ) 0 (f y))
Tactic: apply derivWithin_zero_of_frequently_mem {0, 1} (mt Set.Infinite.of_accPt (by simp))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℂ → ℂ
x : ℂ
hf : DifferentiableAt ℂ f x
c : ℂ
⊢ deriv (fun (x : ℂ) ↦ c ^ f x) x = log c * deriv f x * c ^ f x
have hf₁ : DifferentiableWithinAt ℂ f Set.univ x
Tactic: rw [← derivWithin_univ, derivWithin_const_cpow, derivWithin_univ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ -1
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have hr₁ : r + 1 ≠ 0
Tactic: rw [Ne, ← add_eq_zero_iff_eq_neg, ← Ne] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have inl : ∀ (hx : 0 < x), HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
Tactic: rcases lt_or_gt_of_ne hx.symm with (hx | hx)