θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
θ : ℝ
⊢ toReal ↑θ = θ ↔ -π < θ ∧ θ ≤ π
rw [toReal_coe, toIocMod_eq_self two_pi_pos]
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
ring_nf
no goals
θ : ℝ
⊢ θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
rfl