mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inl
⊢ -↑|toReal 0| = 0

pp: case inr.inr
⊢ -↑|(↑π).toReal| = ↑π

Tactic:
<;>

Goal state after:
case inr.inl
⊢ -↑|toReal 0| = 0

case inr.inr
⊢ -↑|(↑π).toReal| = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 1 = 1

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 1 = 0

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 1 = rexp (log x * y)

pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 0 = 1

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 0 = 0

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ¬↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 0 = rexp (log x * y)

pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 1

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 0

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : ¬↑x = 0
h✝ : ¬x = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y)

Tactic:
<;>

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 1 = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 1 = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 1 = rexp (log x * y)

case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 0 = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 0 = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ¬↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 0 = rexp (log x * y)

case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ¬↑x = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : ¬↑x = 0
h✝ : ¬x = 0
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

pp: case neg
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

pp: case neg
x y : ℝ
hx : 0 ≤ x
h✝ : ¬x = 0
⊢ rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
<;>

Goal state after:
case pos
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

case neg
x y : ℝ
hx : 0 ≤ x
h✝ : ¬x = 0
⊢ rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : y = 0
⊢ x ^ y = 1

pp: case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : ¬y = 0
⊢ x ^ y = 0

pp: case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ x ^ y = rexp (log x * y) * cos (y * π)

Tactic:
<;>

Goal state after:
case pos
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : y = 0
⊢ x ^ y = 1

case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : x = 0
h✝ : ¬y = 0
⊢ x ^ y = 0

case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ x ^ y = rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < x ^ y

Tactic:
by
  rw [rpow_def_of_pos hx]; apply exp_pos

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
h : x = 0
⊢ 0 ^ x ≤ 1

pp: case neg
x : ℝ
h : ¬x = 0
⊢ 0 ^ x ≤ 1

Tactic:
<;>

Goal state after:
case pos
x : ℝ
h : x = 0
⊢ 0 ^ x ≤ 1

case neg
x : ℝ
h : ¬x = 0
⊢ 0 ^ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
h : x = 0
⊢ 0 ≤ 0 ^ x

pp: case neg
x : ℝ
h : ¬x = 0
⊢ 0 ≤ 0 ^ x

Tactic:
<;>

Goal state after:
case pos
x : ℝ
h : x = 0
⊢ 0 ≤ 0 ^ x

case neg
x : ℝ
h : ¬x = 0
⊢ 0 ≤ 0 ^ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 ≤ 1

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 0

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ 0 ≤ rexp (log x * y)

Tactic:
<;>

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 ≤ 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ 0 ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y : ℝ
hx : x = 0
hy : y = 0
⊢ |x| ^ y ≤ rexp (log x * y)

pp: case neg
x y : ℝ
hx : x = 0
hy : ¬y = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
<;>

Goal state after:
case pos
x y : ℝ
hx : x = 0
hy : y = 0
⊢ |x| ^ y ≤ rexp (log x * y)

case neg
x y : ℝ
hx : x = 0
hy : ¬y = 0
⊢ |x| ^ y ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

pp: case inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
<;>

Goal state after:
case inl.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h : ψ.sign = -1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inl
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 0
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

case inl.inr.inr
θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign
h : ψ.sign = 1
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : ¬y = 0
⊢ 1 = 0⁻¹

pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : y = 0
⊢ 0 = 1⁻¹

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ rexp (log x * -y) = (rexp (log x * y))⁻¹

Tactic:
<;>

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : y = 0
⊢ 1 = 1⁻¹

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : -y = 0
h✝ : ¬y = 0
⊢ 1 = 0⁻¹

case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : y = 0
⊢ 0 = 1⁻¹

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : x = 0
h✝¹ : ¬-y = 0
h✝ : ¬y = 0
⊢ 0 = 0⁻¹

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ rexp (log x * -y) = (rexp (log x * y))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ ↑1 = 1

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ ↑0 = 0

pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ ↑(rexp (Real.log x * y)) = cexp (log ↑x * ↑y)

Tactic:
<;>

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : y = 0
⊢ ↑1 = 1

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ ↑0 = 0

case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝ : ¬x = 0
⊢ ↑(rexp (Real.log x * y)) = cexp (log ↑x * ↑y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

Tactic:
rcases eq_or_ne y 0 with (rfl | hy)

Goal state after:
case inl.inl
hx : 0 ≤ 0
⊢ ↑0 ^ 0 = (-↑0) ^ 0 * cexp (↑π * I * 0)

case inl.inr
y : ℂ
hx : 0 ≤ 0
hy : y ≠ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inl
hx : 0 ≤ 0
⊢ ↑0 ^ 0 = (-↑0) ^ 0 * cexp (↑π * I * 0)

pp: case inl.inr
y : ℂ
hx : 0 ≤ 0
hy : y ≠ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

Tactic:
<;>

Goal state after:
case inl.inl
hx : 0 ≤ 0
⊢ ↑0 ^ 0 = (-↑0) ^ 0 * cexp (↑π * I * 0)

case inl.inr
y : ℂ
hx : 0 ≤ 0
hy : y ≠ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case refine_1
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 < c ^ r⁻¹

pp: case refine_2
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ c ^ r⁻¹

pp: case refine_3
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ r

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 < c ^ r⁻¹

case refine_2
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ c ^ r⁻¹

case refine_3
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hr : 0 < r
hg : 0 ≤ᶠ[l] g
h : f =o[l] g
c : ℝ
hc : 0 < c
⊢ 0 ≤ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z w : ℂ
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by
  by_cases! h : z = 0 → w.re = 0 → w = 0
  · exact (norm_cpow_of_imp h).le
  · simp [h]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ ‖x‖ ^ (↑y).re / rexp (x.arg * (↑y).im) = ‖x‖ ^ y

pp: x : ℂ
y : ℝ
⊢ x = 0 → (↑y).re = 0 → ↑y = 0

Tactic:
<;>

Goal state after:
x : ℂ
y : ℝ
⊢ ‖x‖ ^ (↑y).re / rexp (x.arg * (↑y).im) = ‖x‖ ^ y

x : ℂ
y : ℝ
⊢ x = 0 → (↑y).re = 0 → ↑y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x‖ ^ y.re / rexp ((↑x).arg * y.im) = x ^ y.re

pp: x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ↑x = 0 → y.re = 0 → y = 0

Tactic:
<;>

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ‖↑x‖ ^ y.re / rexp ((↑x).arg * y.im) = x ^ y.re

x : ℝ
hx : 0 ≤ x
y : ℂ
hy : y.re ≠ 0
⊢ ↑x = 0 → y.re = 0 → y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₁
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log ↑x * ↑y).im

pp: case h₂
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log ↑x * ↑y).im ≤ π

Tactic:
<;>

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ -π < (Complex.log ↑x * ↑y).im

case h₂
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ (Complex.log ↑x * ↑y).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h✝ : z = 0
⊢ 1 = x ^ z * y ^ z

pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h✝ : ¬z = 0
⊢ 0 = x ^ z * y ^ z

pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x * y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z

Tactic:
<;>

Goal state after:
case pos
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h✝ : z = 0
⊢ 1 = x ^ z * y ^ z

case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : x * y = 0
h✝ : ¬z = 0
⊢ 0 = x ^ z * y ^ z

case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x * y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h✝ : z = 0
⊢ rexp (log (x * y) * z) = 1 * y ^ z

pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h✝ : ¬z = 0
⊢ rexp (log (x * y) * z) = 0 * y ^ z

pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

Tactic:
<;>

Goal state after:
case pos
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h✝ : z = 0
⊢ rexp (log (x * y) * z) = 1 * y ^ z

case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : x = 0
h✝ : ¬z = 0
⊢ rexp (log (x * y) * z) = 0 * y ^ z

case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬x = 0 ∧ ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
y : ℝ
h : y = 0
⊢ 0 ^ y = 1

pp: case neg
y : ℝ
h : ¬y = 0
⊢ 0 ^ y = 0

Tactic:
<;>

Goal state after:
case pos
y : ℝ
h : y = 0
⊢ 0 ^ y = 1

case neg
y : ℝ
h : ¬y = 0
⊢ 0 ^ y = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case ofNat
x : ℝ≥0
a✝ : ℕ
⊢ x ^ ↑(Int.ofNat a✝) = x ^ Int.ofNat a✝

pp: case negSucc
x : ℝ≥0
a✝ : ℕ
⊢ x ^ ↑(Int.negSucc a✝) = x ^ Int.negSucc a✝

Tactic:
<;>

Goal state after:
case ofNat
x : ℝ≥0
a✝ : ℕ
⊢ x ^ ↑(Int.ofNat a✝) = x ^ Int.ofNat a✝

case negSucc
x : ℝ≥0
a✝ : ℕ
⊢ x ^ ↑(Int.negSucc a✝) = x ^ Int.negSucc a✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
x : ℝ≥0
hx_pos : 0 < x
⊢ 0 < x ^ p

Tactic:
by
  have rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p := by
    intro p hp_pos
    rw [← zero_rpow hp_pos.ne']
    exact rpow_lt_rpow hx_pos hp_pos
  rcases lt_trichotomy (0 : ℝ) p with (hp_pos | rfl | hp_neg)
  · exact rpow_pos_of_nonneg hp_pos
  · simp only [zero_lt_one, rpow_zero]
  · rw [← neg_neg p, rpow_neg, inv_pos]
    exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y

pp: case hy
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ z ≠ 0

pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y ^ z⁻¹

Tactic:
<;>

Goal state after:
case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y

case hy
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ z ≠ 0

x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x

pp: case hy
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ z ≠ 0

pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x ^ z⁻¹

Tactic:
<;>

Goal state after:
case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x

case hy
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ z ≠ 0

x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ x ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ y

pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹

Tactic:
<;>

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ y

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (0, z)

Tactic:
ContinuousAt,

Goal state after:
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ x.1 ^ x.2) (𝓝 (0, z)) (𝓝 ((0, z).1 ^ (0, z).2))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ x

pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ z⁻¹

Tactic:
<;>

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ x

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ ‖x ^ y‖₊ = ‖x‖₊ ^ y

Tactic:
by
  ext; exact Real.norm_rpow_of_nonneg hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
⊢ ∞ ^ 0 = 1

pp: case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 0 = 1

Tactic:
<;>

Goal state after:
case top
⊢ ∞ ^ 0 = 1

case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case e'_5
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 0 = ‖(0, z).1‖ ^ (re ∘ Prod.snd) (0, z)

pp: case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ‖(0, z).1‖ ≠ 0 ∨ 0 < (re ∘ Prod.snd) (0, z)

Tactic:
<;>

Goal state after:
case e'_5
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ 0 = ‖(0, z).1‖ ^ (re ∘ Prod.snd) (0, z)

case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ ‖(0, z).1‖ ≠ 0 ∨ 0 < (re ∘ Prod.snd) (0, z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
y : ℝ
H : y < 0
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0

pp: case top.inr.inl
y : ℝ
H : y = 0
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0

pp: case top.inr.inr
y : ℝ
H : 0 < y
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0

Tactic:
<;>

Goal state after:
case top.inl
y : ℝ
H : y < 0
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0

case top.inr.inl
y : ℝ
H : y = 0
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0

case top.inr.inr
y : ℝ
H : 0 < y
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

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

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

Tactic:
· -- x > 0 : easy case
    have : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
    refine (continuousAt_cpow (Or.inl ?_)).comp this
    rwa [ofReal_re]

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ ¬x ^ z ≤ x ^ y ↔ z < y

Tactic:
rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1,

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ ¬y ≤ z ↔ z < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

pp: case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

pp: case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
<;>

Goal state after:
case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
y : ℝ
H : y < 0
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y

pp: case top.inr.inl
y : ℝ
H : y = 0
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y

pp: case top.inr.inr
y : ℝ
H : 0 < y
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y

Tactic:
<;>

Goal state after:
case top.inl
y : ℝ
H : y < 0
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y

case top.inr.inl
y : ℝ
H : y = 0
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y

case top.inr.inr
y : ℝ
H : 0 < y
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inl
hx : 0 ≤ 0
⊢ 0 ^ 0 < 1 ↔ 0 = 0 ∧ 0 ≠ 0 ∨ 1 < 0 ∧ 0 < 0 ∨ 0 < 1 ∧ 0 < 0

pp: case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

Tactic:
<;>

Goal state after:
case inl.inl
hx : 0 ≤ 0
⊢ 0 ^ 0 < 1 ↔ 0 = 0 ∧ 0 ≠ 0 ∨ 1 < 0 ∧ 0 < 0 ∨ 0 < 1 ∧ 0 < 0

case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

pp: case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

pp: case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
<;>

Goal state after:
case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inl
hx : 0 ≤ 0
⊢ 1 < 0 ^ 0 ↔ 1 < 0 ∧ 0 < 0 ∨ 0 < 0 ∧ 0 < 1 ∧ 0 < 0

pp: case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

Tactic:
<;>

Goal state after:
case inl.inl
hx : 0 ≤ 0
⊢ 1 < 0 ^ 0 ↔ 1 < 0 ∧ 0 < 0 ∨ 0 < 0 ∧ 0 < 1 ∧ 0 < 0

case inl.inr
y : ℝ
hx : 0 ≤ 0
hy : ¬y = 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
y : ℝ
H : y < 0
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

pp: case top.inr.inl
y : ℝ
H : y = 0
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

pp: case top.inr.inr
y : ℝ
H : 0 < y
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

Tactic:
<;>

Goal state after:
case top.inl
y : ℝ
H : y < 0
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

case top.inr.inl
y : ℝ
H : y = 0
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹

case top.inr.inr
y : ℝ
H : 0 < y
⊢ ∞ ^ (-y) = (∞ ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

pp: case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

pp: case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
<;>

Goal state after:
case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
y z : ℝ
Hy : y < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inl
y z : ℝ
Hy : y = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inr
y z : ℝ
Hy : 0 < y
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
<;>

Goal state after:
case top.inl
y z : ℝ
Hy : y < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inl
y z : ℝ
Hy : y = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inr
y z : ℝ
Hy : 0 < y
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl.inl
y z : ℝ
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inl.inr.inl
y z : ℝ
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inl.inr.inr
y z : ℝ
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inl.inl
y z : ℝ
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inl.inr.inl
y z : ℝ
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inl.inr.inr
y z : ℝ
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

pp: case top.inr.inr.inr.inr
y z : ℝ
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

Tactic:
<;>

Goal state after:
case top.inl.inl
y z : ℝ
Hy : y < 0
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inl.inr.inl
y z : ℝ
Hy : y < 0
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inl.inr.inr
y z : ℝ
Hy : y < 0
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inl.inl
y z : ℝ
Hy : y = 0
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inl.inr.inl
y z : ℝ
Hy : y = 0
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inl.inr.inr
y z : ℝ
Hy : y = 0
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z < 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inr.inr.inl
y z : ℝ
Hy : 0 < y
Hz : z = 0
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z

case top.inr.inr.inr.inr
y z : ℝ
Hy : 0 < y
Hz : 0 < z
⊢ ∞ ^ (y * z) = (∞ ^ y) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

pp: case pos.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
<;>

Goal state after:
case pos.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y < 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inl
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : y = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case pos.inr.inr
y z : ℝ
x : ℝ≥0
h : x = 0
Hy : 0 < y
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z