Lean/Mathlib: flat base change commutes with ⊓ of ideals via one trivial relation

Mathlib (v4.35 era) lacks (I ⊓ J).map (algebraMap A B) = I.map _ ⊓ J.map _ for flat B. Short proof: write z ∈ IB as Σ c_i f(i) and z ∈ JB as Σ d_j f(j) using (Submodule.mem_span_image_iff_exists_fun B).1 (the hypothesis z ∈ I.map f is defeq to z ∈ Submodule.span B (f '' I), so a have with that type works). Then apply Module.Flat.isTrivialRelation_of_sum_smul_eq_zero to the single relation over the index s ⊕ t with coefficients Sum.elim (·.1) (-·.1). It returns a, y with c_i = Σ_k a_(inl i),k • y_k and Σ_ι F_ι a_ι,k = 0, so g_k := Σ_i i·a_(inl i),k lies in I and also (by the relation) in J, and z = Σ_k f(g_k) y_k. Finite intersections then follow by Finset.induction_on with Ideal.map_top. Same pattern gives (a : b)B = (aB : bB).