TileStructure.Forest.P7_5_4_le_adjointBoundaryOperator_mul

lemma P7_5_4_le_adjointBoundaryOperator_mul (mx : x ∈ ball (c J) (8⁻¹ * D ^ s J)) :    P7_5_4 t u₁ u₂ f₁ f₂ J ≤    adjointBoundaryOperator t u₁ f₁ x * adjointBoundaryOperator t u₂ f₂ x := by  have mx' : x ∈ J := by    refine ((ball_subset_ball ?_).trans ball_subset_Grid) mx    change _ ≤ (D : ℝ) ^ s J / 4; rw [div_eq_inv_mul]; gcongr; norm_num  unfold P7_5_4 adjointBoundaryOperator  conv_lhs => enter [1]; rw [← add_zero (_ + _)]  conv_lhs => enter [2]; rw [← add_zero (_ + _)]  gcongr  exacts [biInf_le _ mx, biInf_le _ mx', zero_le, biInf_le _ mx, biInf_le _ mx', zero_le]