Quanta Wave Number subset brillouin Zone

lemma quantaWaveNumber_subset_brillouinZone : T.QuantaWaveNumber ⊆ T.BrillouinZone := by  rintro _ ⟨n, rfl⟩  have hT := T.a_pos  have hNpos : 0 < T.N := lt_of_le_of_lt (Nat.zero_le _) n.isLt  simp only [BrillouinZone, Set.mem_Ico]  generalize T.N = x at *  generalize T.a = a at *  have hx : (0 : ℝ) < x := by exact_mod_cast hNpos  have hn : (n : ℝ) + 1 ≤ x := by exact_mod_cast n.isLt  have hn0 : (0 : ℝ) ≤ n := by positivity  have hx2 : 2 * ((x / 2 : ℕ) : ℝ) ≤ x := by exact_mod_cast (by omega : 2 * (x / 2) ≤ x)  have hx2' : (x : ℝ) ≤ 2 * ((x / 2 : ℕ) : ℝ) + 1 := by    exact_mod_cast (by omega : x ≤ 2 * (x / 2) + 1)  refine ⟨?_, ?_⟩  · rw [div_mul_eq_mul_div, div_le_div_iff₀ hT (mul_pos hT hx)]    nlinarith [hx2, hn0, mul_pos Real.pi_pos hT]  · rw [div_mul_eq_mul_div, div_lt_div_iff₀ (mul_pos hT hx) hT]    nlinarith [hn, hx2', mul_pos Real.pi_pos hT]