case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toReal ↑x✝) = toReal ↑x✝
θ : Angle
⊢ toIocMod two_pi_pos (-π) (toReal θ) = toReal θ
induction θ using Real.Angle.induction_on
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toReal ↑x✝) = toReal ↑x✝
rw [toReal_coe]
no goals
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
exact toIocMod_toIocMod _ _ _ _