ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
have : Int.natAbs 2 = 2 := rfl
no goals
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
  Fin.val_one, zero_smul, coe_zero, add_zero, one_smul, Int.cast_two,
  mul_div_cancel_left (_ : ℝ) two_ne_zero]