Function.Periodic.ae_of_ae_restrict

lemma Function.Periodic.ae_of_ae_restrict {T : ℝ} (hT : 0 < T) {a : ℝ} {P : (x : ℝ) → Prop}    (hP : Function.Periodic P T)    (h : ∀ᵐ x ∂volume.restrict (Set.Ico a (a + T)), P x) : ∀ᵐ x, P x := by  rw [ae_restrict_iff' measurableSet_Ico, ae_iff] at h  set E_interval := {x | ¬(x ∈ Set.Ico a (a + T) → P x)} with E_interval_def  -- Define exceptional set as countable union of translations of the exceptional set on the interval  set E := ⋃ (k : ℤ), k • T +ᵥ E_interval with Edef  have hE : E = {a | ¬P a} := by    ext x    rw [Set.mem_iUnion]    constructor    · intro h      rcases h with ⟨k, hk⟩      rw [Set.mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, ← sub_eq_neg_add, E_interval_def] at hk      simp only [Classical.not_imp, Set.mem_setOf_eq, hP.sub_zsmul_eq k] at hk      exact hk.2    · dsimp      rcases (hP.exists_mem_Ico' hT x a) with ⟨n, hn, hxn⟩      rw [hxn]      refine fun h ↦ ⟨n, ?_⟩      rw [Set.mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, ← sub_eq_neg_add, E_interval_def]      simp only [Classical.not_imp, Set.mem_setOf_eq]      exact ⟨hn, h⟩  -- The union still has measure zero  have Emeasure : volume E = 0 := by    rw [Edef, measure_iUnion_null]    refine fun k ↦ measure_vadd_null h ..  rw [ae_iff, ← hE]  exact Emeasure