Grid.dist_strictMono

lemma dist_strictMono {I J : Grid X} (hpq : I < J) {f g : Θ X} :    dist_{I} f g ≤ C2_1_2 a * dist_{J} f g := by  calc    _ ≤ dist_{c I, 4 * D ^ s I} f g :=      cdist_mono (ball_subset_ball (by simp_rw [div_eq_inv_mul, defaultD]; gcongr; norm_num))    _ ≤ 2 ^ (-𝕔 * (a : ℝ)) * dist_{c I, 4 * D ^ (s I + 1)} f g := by      rw [← div_le_iff₀' (by positivity), neg_mul, Real.rpow_neg zero_le_two, div_inv_eq_mul, mul_comm]      convert! le_cdist_iterate (x := c I) (r := 4 * D ^ s I) (by positivity) f g (𝕔 * a) using 1      · norm_cast      · apply dist_congr rfl        have : (defaultA a : ℝ) ^ (𝕔 * a) = D := by          simp only [defaultD, Nat.cast_pow, Nat.cast_ofNat]          rw [← pow_mul]; congr 1; ring        rw [this, zpow_add_one₀ (realD_pos a).ne']; ring    _ ≤ 2 ^ (-𝕔 * (a : ℝ)) * dist_{c I, 4 * D ^ s J} f g := by      gcongr      have : s I < s J := (Grid.lt_def.mp hpq).2      apply cdist_mono      gcongr      · exact one_le_realD _      · lia    _ ≤ 2 ^ (-𝕔 * (a : ℝ)) * dist_{c J, 8 * D ^ s J} f g := by      gcongr      have : c I ∈ ball (c J) (4 * D ^ s J) :=        mem_of_mem_of_subset c_mem_Grid ((Grid.lt_def.mp hpq).1.trans Grid_subset_ball)      rw [mem_ball] at this      exact cdist_mono (ball_subset_ball' (by linarith))    _ ≤ 2 ^ (-𝕔 * (a : ℝ) + 5 * a) * dist_{J} f g := by      rw [Real.rpow_add zero_lt_two, mul_assoc]      gcongr      rw [show (2 : ℝ) ^ (5 * (a : ℝ)) = (defaultA a) ^ 5 by norm_cast; ring]      convert! cdist_le_iterate _ f g 5 using 1      · exact dist_congr rfl (by ring)      · have := one_le_realD a; positivity    _ = _ := by congr 1; rw [C2_1_2, ← add_mul]