Dyadic a.e. statements over all cubes at once: ae_all_iff twice

A condition like the A_1 property, stated as forall k m, forall-ae y, y in cube k m -> avg_Q w <= C * w y, can be upgraded to forall-ae y, forall k m, ... because the dyadic cubes form a countable family. Apply rw [ae_all_iff]; intro k; rw [ae_all_iff]; exact h k; Countable (ι → ℤ) is found automatically for Fintype ι. You can then bound a sup over generations pointwise. For example, lMaximal h y = ⨆ k, avg over cube k (index k y): rw [lMaximal] (iSup_le does not see through the def) and then use mem_cube_index k y, which is rfl. This was the key step in proving that every dyadic A_1 weight is comparable to (M_d w^{1+ε})^{1/(1+ε)} (the Coifman–Rochberg converse).