θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ abs (toReal (-↑θ)) = θ
θ : ℝ
⊢ abs (toReal (-↑θ)) = θ ↔ 0 ≤ θ ∧ θ ≤ π
refine' ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => _⟩
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ abs (toReal (-↑θ)) = θ

case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ abs (toReal (-↑θ)) = θ
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ abs (toReal (-↑θ)) = θ
by_cases hnegpi : θ = π
no goals
case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ abs (toReal (-↑θ)) = θ
rw [← coe_neg,
  toReal_coe_eq_self_iff.2
    ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
  abs_neg, abs_eq_self.2 h.1]
no goals
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ abs (toReal (-↑θ)) = θ
simp [hnegpi, Real.pi_pos.le]