θ : Angle
⊢ abs (toReal θ) ≤ π / 2 → (abs (toReal θ) ≠ π / 2 ↔ 0 ≠ cos θ)
θ : Angle
⊢ 0 < cos θ ↔ abs (toReal θ) < π / 2
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, cos_nonneg_iff_abs_toReal_le_pi_div_two, ←
  and_congr_right]
θ : Angle
⊢ abs (toReal θ) ≠ π / 2 ↔ 0 ≠ cos θ
θ : Angle
⊢ abs (toReal θ) ≤ π / 2 → (abs (toReal θ) ≠ π / 2 ↔ 0 ≠ cos θ)
rintro -
no goals
θ : Angle
⊢ abs (toReal θ) ≠ π / 2 ↔ 0 ≠ cos θ
rw [Ne.def, Ne.def, not_iff_not, @eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]