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

Goal state before:
pp: case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ ↑a ^ r * ↑b ^ r = ↑a ^ r * ↑b ^ r

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
]

Goal state after:
z : ℂ
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
⊢ ↑θ = ↑ψ

Tactic:
]

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ↔ 0 ≤ z.re

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
]

Goal state after:
z : ℂ
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ

Tactic:
]

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n * 2 + 1 = 0
this : 1 % 2 = 0 % 2
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
]

Goal state after:
θ : Angle
⊢ θ.sin = sin 0 ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π

Tactic:
]

Goal state after:
θ : Angle
⊢ θ = 0 ∨ θ + 0 = ↑π ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sin ≠ 0 ↔ ¬θ.sin = 0

Tactic:
]

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

Goal state before:
pp: x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π

Tactic:
]

Goal state after:
x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: ⊢ -1 = -1

Tactic:
]

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

Goal state before:
pp: x : ℂ
hi : x.im < 0
⊢ Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π

Tactic:
]

Goal state after:
x : ℂ
hi : x.im < 0
⊢ Real.arccos ((-x).re / ‖-x‖) = -Real.arccos (x.re / ‖x‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
]

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

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ ↑a ^ r * (↑b ^ r)⁻¹ = ↑a ^ r * (↑b ^ r)⁻¹

Tactic:
]

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

Goal state before:
pp: x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n

Tactic:
]

Goal state after:
x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
]

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

Goal state before:
pp: θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.sin| = |ψ.sin|

Tactic:
]

Goal state after:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.sin| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

Tactic:
]

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

Goal state before:
pp: case inr
ψ : Angle
⊢ |ψ.sin| = |ψ.sin|

Tactic:
]

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

Goal state before:
pp: θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.cos| = |ψ.cos|

Tactic:
]

Goal state after:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ |θ.cos| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
ψ : Angle
⊢ |ψ.cos| = |ψ.cos|

Tactic:
]

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

Goal state before:
pp: θ ψ : ℝ
⊢ ∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Tactic:
]

Goal state after:
θ ψ : ℝ
⊢ ∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ) = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)

Tactic:
]

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

Goal state before:
pp: θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Tactic:
]

Goal state after:
θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ 2 * π * ↑(-toIocDiv two_pi_pos ψ θ) = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)

Tactic:
]

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

Goal state before:
pp: θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π

Tactic:
]

Goal state after:
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hi : x.im = 0
⊢ (-↑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
x : ℂ
hi : x.im = 0
⊢ (-↑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: θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ θ ∈ Set.Ioc (-π) π

Tactic:
]

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

Goal state before:
pp: case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝

Tactic:
]

Goal state after:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ -π < 0 ∧ 0 ≤ π

Tactic:
]

Goal state after:
⊢ -π < 0 ∧ 0 ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0

Tactic:
]

Goal state after:
θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ -π < π ∧ π ≤ π

Tactic:
]

Goal state after:
⊢ -π < π ∧ π ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π ↔ θ.toReal = π

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ ↑π

Tactic:
]

Goal state after:
θ : Angle
⊢ -π < -θ.toReal ∧ -θ.toReal ≤ π ↔ θ ≠ ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
]

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

Goal state before:
pp: case mpr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π

Tactic:
]

Goal state after:
case mpr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal < π ∧ -θ.toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ π ≠ 0

Tactic:
]

Goal state after:
⊢ π ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal = π / 2 ↔ θ.toReal = π / 2

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal = -π / 2 ↔ θ.toReal = -π / 2

Tactic:
]

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

Goal state before:
pp: ⊢ π / 2 ≠ 0

Tactic:
]

Goal state after:
⊢ π / 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ -π / 2 ≠ 0

Tactic:
]

Goal state after:
⊢ -π / 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ θ = θ

Tactic:
]

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

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

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n) = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)

Tactic:
]

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

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

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ x ^ (starRingEnd ℂ) n = x ^ (starRingEnd ℂ) n

Tactic:
]

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π ↔ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2) ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
]

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

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π

Tactic:
]

Goal state after:
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inr.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
⊢ ↑(-↑x.re).arg = ↑(↑x.re).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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
]

Goal state after:
θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
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
⊢ ↑π = ↑π

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal

Tactic:
]

Goal state after:
θ : Angle
⊢ π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ 3 * π ↔ π / 2 < θ.toReal
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:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ π / 2 < θ.toReal ↔ π / 2 < θ.toReal

Tactic:
]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
]

Goal state after:
θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2

Tactic:
]

Goal state after:
θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
]

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: θ : ℝ
⊢ 2 * π * ↑⌊(π - θ) / (2 * π)⌋ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
]

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

Goal state before:
pp: θ : Real.Angle
⊢ θ = θ

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal ≤ -π / 2 ↔ θ.toReal ≤ -π / 2

Tactic:
]

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

Goal state before:
pp: θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ Real.cos |θ.toReal| ↔ |θ.toReal| ≤ π / 2

Tactic:
]

Goal state after:
θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ Real.cos |θ.toReal| ↔ |θ.toReal| ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = x * y

Tactic:
]

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑x.arg + -↑y.arg = ↑x.arg + -↑y.arg

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ |θ.toReal| ≤ π / 2 ∧ ?m.30 ↔ |θ.toReal| ≤ π / 2 ∧ |θ.toReal| ≠ π / 2

pp: θ : Angle
⊢ |θ.toReal| ≤ π / 2 → (?m.30 ↔ 0 ≠ θ.cos)

pp: θ : Angle
⊢ Prop

Tactic:
]

Goal state after:
θ : Angle
⊢ |θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
]

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

Goal state before:
pp: z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
]

Goal state after:
z : ℂ
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
θ : Real.Angle
⊢ z.arg = θ.toReal ↔ z.arg = θ.toReal

Tactic:
]

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

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x.arg + y.arg ∈ Ioc (-π) π ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
]

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

Goal state before:
pp: θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
]

Goal state after:
θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |θ.cos| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: x : ℝ
⊢ Real.sin x / Real.cos x = Real.sin x / Real.cos x

Tactic:
]

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

Goal state before:
pp: x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0

Tactic:
]

Goal state after:
x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝

Tactic:
]

Goal state after:
case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x

Tactic:
]

Goal state after:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ θ.tan = ψ.tan

Tactic:
]

Goal state after:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ θ.tan = ψ.tan
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
]

Goal state after:
case h.h
x✝¹ x✝ : ℝ
h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
]

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = Real.arcsin ((-a✝).im / ‖a✝‖) - π

Tactic:
]

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

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan (π / 2 - x✝¹ + ↑k * π) = Real.tan (π / 2 - x✝¹)

Tactic:
]

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan (π / 2 - x✝¹ + ↑k * π) = Real.tan (π / 2 - x✝¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ SignType.sign (sin 0) = 0

Tactic:
sin_zero,

Goal state after:
⊢ SignType.sign 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -SignType.sign θ.sin = -SignType.sign θ.sin

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ -θ.sign = -θ.sign

Tactic:
]

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

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) + π = Real.arcsin ((-a✝).im / ‖a✝‖) + π

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ.sign ≠ 0 ↔ ¬θ.sign = 0

Tactic:
]

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Tactic:
]

Goal state after:
θ : Angle
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0
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‖) + π
⊢ Real.arcsin ((-z).im / ‖z‖) + π = Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: θ : Angle
h : 0 ≤ θ.sign
⊢ θ = θ

Tactic:
]

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

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

Tactic:
]

Goal state after:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
⊢ -↑|θ.toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = ↑x.arg + ↑π

Tactic:
]

Goal state after:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
⊢ ContinuousAt (fun z ↦ ↑z.arg + ↑π) (-x)

Tactic:
]

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
⊢ ContinuousAt (fun z ↦ ↑z.arg + ↑π) (-x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin

Tactic:
]

Goal state after:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0

Tactic:
]

Goal state after:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ x.re < 0