mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (x + y) / x

pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x

pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y

Tactic:
one_add_div

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ (x + y) / x = (x + y) / x

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ x ≠ 0

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|

Tactic:
;

Goal state after:
x : ℂ
⊢ |if x.arg = π then π else -x.arg| = |x.arg|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x✝ : ℂ
⊢ x✝ ∈ (fun θ ↦ cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1

Tactic:
;

Goal state after:
x✝ : ℂ
⊢ x✝ ∈ (fun θ ↦ cexp (↑θ * I)) '' Ioc (-π) π ↔ x✝ ∈ sphere 0 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

pp: case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ

Tactic:
;

Goal state after:
case inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ

Tactic:
;

Goal state after:
case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).cos = -(↑x✝).sin

Tactic:
exact Real.cos_add_pi_div_two _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-↑θ).toReal| = θ

pp: case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-↑θ).toReal| = θ

Tactic:
;

Goal state after:
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-↑θ).toReal| = θ

case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-↑θ).toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False

Tactic:
;

Goal state after:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
;

Goal state after:
θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re =
    if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.«0»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = -(2 * π) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
;

Goal state after:
case inr.«0»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = -(2 * π) + π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x : ℝ
hx : x ≤ 0
y : ℝ
h : ¬x = 0
⊢ (↑x ^ ↑y).re = rexp (log x * y) * cos (y * π)

Tactic:
;

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

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < rexp (log x * y)

Tactic:
;

Goal state after:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 0) x✝ = 1 x✝

Tactic:
;

Goal state after:
α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 0) x✝ = 1 x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case inr.inl
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (𝓝 0)

pp: case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)

Tactic:
case inr.inl => -- b = 0
    refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
    rw [tendsto_pure]
    filter_upwards [eventually_ne_atTop 0] with _ hx
    simp [hx]

Goal state after:
case inr.inr
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (fun x ↦ b ^ x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.«1»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π

Tactic:
;

Goal state after:
case inr.«1»
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
hk : θ.toReal + ψ.toReal = π
⊢ θ.toReal + ψ.toReal = π ∨ θ.toReal + ψ.toReal = -π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 1) x✝ = f x✝

Tactic:
;

Goal state after:
α : Type u_1
f : α → ℝ
x✝ : α
⊢ (f ^ 1) x✝ = f x✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
;

Goal state after:
w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ (f i + ∑ x ∈ s, f x) = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
prod_cons,

Goal state after:
case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ (f i + ∑ x ∈ s, f x) = a ^ f i * ∏ x ∈ s, a ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ (if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) =
    (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log ↑x * ↑y)

Tactic:
;

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log ↑x * ↑y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case h₁
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ |f x| ≤ c * |g x|

Tactic:
;

Goal state after:
case h₁
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
x : α
hgx : 0 x ≤ g x
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ |f x| ≤ c * |g x|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
;

Goal state after:
x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).re = ‖x‖ ^ y * Real.cos (x.arg * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).re = ‖x‖ ^ y * Real.cos z

Tactic:
;

Goal state after:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).re = ‖x‖ ^ y * Real.cos z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).im = ‖x‖ ^ y * Real.sin (x.arg * y)

Tactic:
;

Goal state after:
x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).im = ‖x‖ ^ y * Real.sin (x.arg * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).im = ‖x‖ ^ y * Real.sin z

Tactic:
;

Goal state after:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).im = ‖x‖ ^ y * Real.sin z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x ^ ↑(↑n)⁻¹‖

Tactic:
;

Goal state after:
x : ℂ
n : ℕ
⊢ ‖x ^ (↑n)⁻¹‖ = ‖x ^ ↑(↑n)⁻¹‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π

Tactic:
;

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 < π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 ≤ π

Tactic:
;

Goal state after:
case h₂
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ 0 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z

pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
;

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (if x * y = 0 then if z = 0 then 1 else 0 else rexp (log (x * y) * z)) = x ^ z * y ^ z

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z

pp: case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
;

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
⊢ 0 < 1

Tactic:
;

Goal state after:
x : ℝ≥0
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = log (x ^ y)

Tactic:
;

Goal state after:
x y : ℝ
hx : 0 < x
hz : 0 < x ^ y
⊢ y * log x = log (x ^ y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
;

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℤ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
;

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
;

Goal state after:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
;

Goal state after:
y : ℝ
n : ℤ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
;

Goal state after:
y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z

Tactic:
;

Goal state after:
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
;

Goal state after:
y : ℝ
n : ℤ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
;

Goal state after:
y : ℝ
n : ℕ
h : y - ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z

pp: case inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z

Tactic:
;

Goal state after:
case inl
x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z

case inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr.inl
x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

pp: case inr.inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z

Tactic:
;

Goal state after:
case inr.inl
x y : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₁' : x < y
h₂ : 0 ≤ 0
⊢ x ^ 0 ≤ y ^ 0

case inr.inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
h₂' : 0 < z
⊢ x ^ z ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ↑(x ^ (y + z)) = ↑(x ^ y * x ^ z)

Tactic:
;

Goal state after:
x : ℝ≥0
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ↑(x ^ (y + z)) = ↑(x ^ y * x ^ z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
;

Goal state after:
case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map ((fun x ↦ x ^ r) ∘ f) l).prod

Tactic:
;

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map ((fun x ↦ x ^ r) ∘ f) l).prod
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ 1) x

Tactic:
;

Goal state after:
case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ 1) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun x ↦ x ^ y) ⋯ (fun x ↦ x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun x ↦ x ^ (1 / y)) ⋯ (fun x ↦ x ^ y) ⋯

Tactic:
;

Goal state after:
y : ℝ
hy : 0 < y
⊢ (StrictMono.orderIsoOfRightInverse (fun x ↦ x ^ y) ⋯ (fun x ↦ x ^ (1 / y)) ⋯).symm =
    StrictMono.orderIsoOfRightInverse (fun x ↦ x ^ (1 / y)) ⋯ (fun x ↦ x ^ y) ⋯
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
;

Goal state after:
x y : ℝ
hx : 0 ≤ x
⊢ ↑‖x ^ y‖₊ = ↑(‖x‖₊ ^ y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < 1

Tactic:
;

Goal state after:
x : ℝ≥0∞
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z

Tactic:
;

Goal state after:
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z

Tactic:
;

Goal state after:
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case ha
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ 0 ≤ log x

Tactic:
;

Goal state after:
case ha
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ 0 ≤ log x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z

Tactic:
;

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z

Tactic:
;

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: 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) ?_)

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

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
by
  rw [← one_rpow z]
  gcongr

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

Goal state before:
pp: x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ≤ x ^ z

Tactic:
by
  rw [← one_rpow z]
  gcongr

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

Goal state before:
pp: case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ 0 < 0 then ∞ else x ^ 0 * y ^ 0

pp: case inr
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
;

Goal state after:
case inl
x y : ℝ≥0∞
⊢ (x * y) ^ 0 = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ 0 < 0 then ∞ else x ^ 0 * y ^ 0

case inr
x y : ℝ≥0∞
z : ℝ
hz : z ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
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 ^ 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 ^ z⁻¹

Tactic:
;

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.coe.top
z : ℝ
hz : z < 0 ∨ 0 < z
x✝ : ℝ≥0
hx0 : ↑x✝ ≠ 0
hy0 : ∞ ≠ 0
hxy : ↑x✝ ≤ ∞
⊢ (↑x✝ * ∞) ^ z = if (↑x✝ = 0 ∧ ∞ = ∞ ∨ ↑x✝ = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * ∞ ^ z

pp: case inr.inr.coe.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝¹ : ℝ≥0
hx0 : ↑x✝¹ ≠ 0
x✝ : ℝ≥0
hy0 : ↑x✝ ≠ 0
hxy : ↑x✝¹ ≤ ↑x✝
⊢ (↑x✝¹ * ↑x✝) ^ z = if (↑x✝¹ = 0 ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z

Tactic:
· rw [ne_eq, coe_eq_zero] at hx0
    rcases hz with hz | hz <;> simp [*]

Goal state after:
case inr.inr.coe.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝¹ : ℝ≥0
hx0 : ↑x✝¹ ≠ 0
x✝ : ℝ≥0
hy0 : ↑x✝ ≠ 0
hxy : ↑x✝¹ ≤ ↑x✝
⊢ (↑x✝¹ * ↑x✝) ^ z = if (↑x✝¹ = 0 ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹

pp: case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
;

Goal state after:
case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹

case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

pp: case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
;

Goal state after:
case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ∞ ≠ 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

pp: case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
;

Goal state after:
case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ∞ ≠ 0
⊢ ∞⁻¹ ^ y = (∞ ^ y)⁻¹

case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ log x ≤ x ^ ε / ε

Tactic:
le_div_iff₀' hε

Goal state after:
case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) a✝¹ ≤ (fun x ↦ 1 ^ x) b✝

Tactic:
;

Goal state after:
hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) a✝¹ ≤ (fun x ↦ 1 ^ x) b✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) b✝ ≤ (fun x ↦ 1 ^ x) a✝¹

Tactic:
;

Goal state after:
hb₀ : 0 < 1
hb₁ : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ 1 ^ x) b✝ ≤ (fun x ↦ 1 ^ x) a✝¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0

Tactic:
;

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0

Tactic:
;

Goal state after:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p

Tactic:
;

Goal state after:
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ (a + b) ^ p ≤ (max a b + max a b) ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p

Tactic:
;

Goal state after:
case h₂
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ max (a ^ p) (b ^ p) ≤ a ^ p + b ^ p