BohrSet.le_iff_width

lemma le_iff_width {B₁ B₂ : BohrSet G} : B₁ ≤ B₂ ↔    B₂.frequencies ⊆ B₁.frequencies ∧ ∀ ⦃ψ⦄, ψ ∈ B₂.frequencies → B₁.width ψ ≤ B₂.width ψ := by  constructor  case mp =>    intro h    refine ⟨frequencies_anti h, fun ψ hψ => ?_⟩    rw [←ENNReal.coe_le_coe, coe_width hψ, coe_width (frequencies_anti h hψ)]    exact h ψ  case mpr =>    rintro ⟨h₁, h₂⟩ ψ    by_cases ψ ∈ B₂.frequencies    case neg h' => simp [ewidth_eq_top_of_not_mem_frequencies h']    case pos h' =>      rw [←coe_width h', ←coe_width (h₁ h'), ENNReal.coe_le_coe]      exact h₂ h'