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

Goal state before:
pp: case inl
⊢ |(-↑π).toReal| = |(↑π).toReal|

pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ |(-θ).toReal| = |θ.toReal|

Tactic:
·

Goal state after:
case inl
⊢ |(-↑π).toReal| = |(↑π).toReal|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ |(-θ).toReal| = |θ.toReal|

Tactic:
·

Goal state after:
case inr
θ : Angle
h : θ ≠ ↑π
⊢ |(-θ).toReal| = |θ.toReal|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
·

Goal state after:
case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
·

Goal state after:
case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re
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| = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
⊢ (n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
have h' : 0 < (n : ℝ) := mod_cast Nat.pos_of_ne_zero h

Goal state after:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ (n • ↑θ.toReal).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

Tactic:
·

Goal state after:
case inr.inr
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

pp: case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

pp: case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
·

Goal state after:
case inl
x : ℂ
hx : x ≠ 0
hi : x.im < 0
⊢ ↑(-x).arg = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-x).arg = ↑x.arg + ↑π

pp: case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
·

Goal state after:
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-x).arg = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

pp: case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

pp: case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
·

Goal state after:
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

pp: case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
·

Goal state after:
case inr.inl.inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π

Tactic:
·

Goal state after:
case inr.inl.inr.inr
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : 0 < x.re
⊢ ↑(-↑x.re).arg = ↑(↑x.re).arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π

Tactic:
·

Goal state after:
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑(-x).arg = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
n : ℕ
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

pp: case inr
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ ↑(x ^ n).arg = n • ↑x.arg

Tactic:
·

Goal state after:
case inl
n : ℕ
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
n : ℕ
⊢ ↑(0 ^ n).arg = n • ↑(arg 0)

Tactic:
by_cases n0 : n = 0 <;> simp [n0]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ ↑(x ^ n).arg = n • ↑x.arg

Tactic:
·

Goal state after:
case inr
x : ℂ
n : ℕ
x0 : x ≠ 0
⊢ ↑(x ^ n).arg = n • ↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ 2 • θ = 2 • ψ ↔ θ = ψ

Tactic:
by
  simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two hθ hψ]

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

Goal state before:
pp: case inl
θ : Angle
⊢ θ.tan = θ.tan

pp: case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan

Tactic:
·

Goal state after:
case inl
θ : Angle
⊢ θ.tan = θ.tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan

Tactic:
·

Goal state after:
case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a ↦ ‖a‖)) z - π)

pp: case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
·

Goal state after:
case e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a ↦ ‖a‖)) z - π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
·

Goal state after:
case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt (fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z | 0 ≤ z.im} z

pp: case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
·

Goal state after:
case refine_1
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ ContinuousWithinAt (fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π) {z | 0 ≤ z.im} z
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
·

Goal state after:
case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal < 0
⊢ SignType.sign θ.toReal = θ.sign

pp: case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal = 0
⊢ SignType.sign θ.toReal = θ.sign

pp: case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
·

Goal state after:
case inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal < 0
⊢ SignType.sign θ.toReal = θ.sign
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal = 0
⊢ SignType.sign θ.toReal = θ.sign

pp: case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
·

Goal state after:
case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal = 0
⊢ SignType.sign θ.toReal = θ.sign
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
·

Goal state after:
case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
⊢ (↑π).toReal ∈ Set.Ioo 0 π ↔ (↑π).sign = 1

pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
·

Goal state after:
case inl
⊢ (↑π).toReal ∈ Set.Ioo 0 π ↔ (↑π).sign = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
·

Goal state after:
case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
·

Goal state after:
case pos
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
·

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ : Angle
h : θ.sign = -1
⊢ -↑|θ.toReal| = θ

pp: case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ

Tactic:
·

Goal state after:
case inl
θ : Angle
h : θ.sign = -1
⊢ -↑|θ.toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ

Tactic:
·

Goal state after:
case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π → a = b

pp: case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π

Tactic:
·

Goal state after:
case mp
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b ∨ a = b + ↑π → a = b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h1 : a = b
⊢ a = b

pp: case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b

Tactic:
·

Goal state after:
case mp.inl
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h1 : a = b
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b

Tactic:
·

Goal state after:
case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π

Tactic:
·

Goal state after:
case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = 0
⊢ |θ.toReal| + |ψ.toReal| = π

pp: case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
·

Goal state after:
case inl
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : θ + ψ = 0
⊢ |θ.toReal| + |ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)

pp: case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0

Tactic:
·

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
k : ℤ
hk : θ.toReal + ψ.toReal = 2 * π * ↑k + π
⊢ 2 * π * ↑k ∈ Set.Ioo (2 * π * ↑(-1 - 1)) (2 * π * ↑(0 + 1))

Tactic:
grind [toReal_mem_Ioc]

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

Goal state before:
pp: case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0

Tactic:
·

Goal state after:
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

pp: case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
·

Goal state after:
case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
·

Goal state after:
case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
·

Goal state after:
case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
·

Goal state after:
case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case mpr.inl
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0

pp: case mpr.inr
⊢ 0 ^ 0 = 1

Tactic:
·

Goal state after:
case mpr.inl
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case mpr.inr
⊢ 0 ^ 0 = 1

Tactic:
·

Goal state after:
case mpr.inr
⊢ 0 ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y

pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
·

Goal state after:
case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
·

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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

Tactic:
·

Goal state after:
case pos
x y : ℝ
hx : x = 0
⊢ |x| ^ y ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
·

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

Goal state before:
pp: case calc.step.inl
x : ℝ
hx : |x| = 0
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

pp: case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
·

Goal state after:
case calc.step.inl
x : ℝ
hx : |x| = 0
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
·

Goal state after:
case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

pp: case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
·

Goal state after:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

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

Tactic:
·

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

Goal state before:
pp: case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
·

Goal state after:
case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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

Tactic:
·

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

Goal state before:
pp: case inl
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

pp: case inr
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
·

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

pp: case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
·

Goal state after:
case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
·

Goal state after:
case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
·

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

Goal state before:
pp: case inr
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
·

Goal state after:
case inr
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : a = ∞
⊢ ↑x < a ^ y

pp: case neg
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : ¬a = ∞
⊢ ↑x < a ^ y

Tactic:
·

Goal state after:
case pos
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
ha' : a = ∞
⊢ ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : (θ + ψ).toReal ≤ 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

pp: case inr
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
·

Goal state after:
case inl
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : (θ + ψ).toReal ≤ 0
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : (θ + ψ).toReal ≤ 0
⊢ 2 * π * ↑k ∈ Set.Ioo (2 * π * ↑(-1 - 1)) (2 * π * ↑(-1 + 1))

Tactic:
grind [toReal_mem_Ioc]

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

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

pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
·

Goal state after:
case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
·

Goal state after:
case inr
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

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 inl
θ ψ : 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 inr
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r

pp: α✝ : Type u_1
r✝ : ℝ
l✝ : Filter α✝
f✝ g✝ : α✝ → ℝ
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
hr : r ≥ 0
⊢ (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r

Tactic:
·

Goal state after:
case inr
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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 inl
y : ℝ
⊢ 0 ^ ↑y = ↑(‖0‖ ^ y) * (↑(Real.cos (arg 0 * y)) + ↑(Real.sin (arg 0 * y)) * I)