mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
·

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ^ ↑y = ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

pp: case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
·

Goal state after:
case inr.inl
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
·

Goal state after:
case inr.inr
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0

pp: case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) atTop (𝓝 ‖a‖)

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) atTop (𝓝 ‖a‖)

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n ↦ g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x ↦ ‖g x‖) / fun n ↦ ↑n ^ r) atTop (𝓝 ‖a‖)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
·

Goal state after:
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

Tactic:
·

Goal state after:
case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

pp: case neg
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
·

Goal state after:
case pos
z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

pp: case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
·

Goal state after:
case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
·

Goal state after:
case neg
z w : ℂ
h : z = 0 ∧ w.re = 0 ∧ w ≠ 0
⊢ ‖z ^ w‖ ≤ ‖z‖ ^ w.re / rexp (z.arg * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
·

Goal state after:
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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

Tactic:
·

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
·

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

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = 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✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

pp: case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

pp: case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
·

Goal state after:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
·

Goal state after:
case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b
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
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
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map ((fun x ↦ x ^ r) ∘ f) l).prod

pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x

Tactic:
·

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
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 inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2)) p

Tactic:
·

Goal state after:
case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x ↦ rexp (log x.1 * x.2)) p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p

pp: case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0

pp: case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p

Tactic:
·

Goal state after:
case inl
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_pos : 0 < p
⊢ 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0

pp: case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p

Tactic:
·

Goal state after:
case inr.inl
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
⊢ 0 < x ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p

Tactic:
·

Goal state after:
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

pp: case inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (0, y)

Tactic:
·

Goal state after:
case inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥

pp: case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x

Tactic:
·

Goal state after:
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
y z : ℝ
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)

pp: case inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
·

Goal state after:
case inl
y z : ℝ
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.inl
y : ℝ
⊢ 0 ^ y = 0 ^ 0 ↔ y = 0 ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ 0 = 0)

pp: case inl.inr
y z : ℝ
hz : z ≠ 0
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
·

Goal state after:
case inl.inl
y : ℝ
⊢ 0 ^ y = 0 ^ 0 ↔ y = 0 ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ 0 = 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl.inr
y z : ℝ
hz : z ≠ 0
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
·

Goal state after:
case inl.inr
y z : ℝ
hz : z ≠ 0
⊢ 0 ^ y = 0 ^ z ↔ y = z ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ z = 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rw [← rpow_le_rpow_iff _ hy hz, rpow_inv_rpow] <;> positivity

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

Goal state before:
pp: case inr.inl
y z : ℝ
hx₀ : 1 ≠ 0
⊢ 1 ^ y = 1 ^ z ↔ y = z ∨ 1 = 1 ∨ 1 = 0 ∧ (y = 0 ↔ z = 0)

pp: case inr.inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
·

Goal state after:
case inr.inl
y z : ℝ
hx₀ : 1 ≠ 0
⊢ 1 ^ y = 1 ^ z ↔ y = z ∨ 1 = 1 ∨ 1 = 0 ∧ (y = 0 ↔ z = 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x ↦ x ^ q) x

pp: case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ x ^ 0) x

Tactic:
·

Goal state after:
case inl
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x ↦ x ^ q) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
·

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

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

pp: case refine_2
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)))

Tactic:
·

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

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

Tactic:
·

Goal state after:
case top
⊢ ∞ ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
·

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

Goal state before:
pp: case refine_2
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)))

Tactic:
·

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

Goal state before:
pp: case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

pp: case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞

pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
·

Goal state after:
case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞

pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
·

Goal state after:
case inr.inl
⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
·

Goal state after:
case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑(x ^ y) = ↑x ^ y

pp: case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
·

Goal state after:
case pos
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
⊢ ↑(x ^ y) = ↑x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑(x ^ y) = ↑x ^ y

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

Tactic:
·

Goal state after:
case pos.inl
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 = y
⊢ ↑(x ^ y) = ↑x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
·

Goal state after:
case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑(x ^ y) = ↑x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
·

Goal state after:
case neg
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : ¬x = 0
⊢ ↑(x ^ y) = ↑x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

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

Tactic:
·

Goal state after:
case top
⊢ ∞ ^ 1 = ∞
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
·

Goal state after:
case coe
x✝ : ℝ≥0
⊢ ↑x✝ ^ 1 = ↑x✝
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:
·

Goal state after:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ
⊢ 1 ^ x = 1

Tactic:
by
  rw [← coe_one, ← coe_rpow_of_ne_zero one_ne_zero]
  simp

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

Goal state before:
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:
·

Goal state after:
case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (0, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
·

Goal state after:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
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:
·

Goal state after:
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.NNReal

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
·

Goal state after:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

pp: case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
·

Goal state after:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

pp: case hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ cexp (↑π * I * p.2)) (x, y)

Tactic:
·

Goal state after:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ (-↑p.1) ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
·

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

Goal state before:
pp: case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
·

Goal state after:
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
·

Goal state after:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ cexp (↑π * I * p.2)) (x, y)

Tactic:
·

Goal state after:
case hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ cexp (↑π * I * p.2)) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

pp: case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
·

Goal state after:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
·

Goal state after:
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z

pp: case coe
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
x✝ : ℝ≥0
⊢ ↑x✝ ^ (y + z) = ↑x✝ ^ y * ↑x✝ ^ z

Tactic:
·

Goal state after:
case top
y z : ℝ
hy : 0 ≤ y
hz : 0 ≤ z
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
⊢ 0 ^ y ≤ 0 ^ z

pp: case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z

Tactic:
·

Goal state after:
case inl
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
⊢ 0 ^ y ≤ 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = ∞ ^ 0 * ∞ ^ z

pp: case top.inr
y z : ℝ
hy✝ : 0 ≤ y
hz : 0 ≤ z
hy : 0 < y
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z

Tactic:
·

Goal state after:
case top.inl
z : ℝ
hz : 0 ≤ z
hy : 0 ≤ 0
⊢ ∞ ^ (0 + z) = ∞ ^ 0 * ∞ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z

pp: case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
·

Goal state after:
case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z

Tactic:
·

Goal state after:
case inl.inr
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
hy0 : y ≠ 0
⊢ 0 ^ y ≤ 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case refine_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (↑(x, y).1, (x, y).2)

pp: case refine_2
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)

Tactic:
·

Goal state after:
case refine_1
x : ℝ≥0
y : ℝ
h : x ≠ 0 ∨ 0 < y
this : (fun p ↦ p.1 ^ p.2) = toNNReal ∘ (fun p ↦ p.1 ^ p.2) ∘ fun p ↦ (↑p.1, p.2)
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (↑(x, y).1, (x, y).2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ∞ ^ (y + 0) = ∞ ^ y * ∞ ^ 0

pp: case top.inr.inr
y z : ℝ
hy✝ : 0 ≤ y
hz✝ : 0 ≤ z
hy : 0 < y
hz : 0 < z
⊢ ∞ ^ (y + z) = ∞ ^ y * ∞ ^ z

Tactic:
·

Goal state after:
case top.inr.inl
y : ℝ
hy✝ : 0 ≤ y
hy : 0 < y
hz : 0 ≤ 0
⊢ ∞ ^ (y + 0) = ∞ ^ y * ∞ ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z

Tactic:
·

Goal state after:
case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z