Moving lemma for Dedekind domains is extractable from IsDedekindDomain.exists_sup_span_eq

Mathlib has no lemma 'every ideal class contains an ideal coprime to a given nonzero ideal', but you can get it from IsDedekindDomain.exists_sup_span_eq (hIJ : I ≤ J) (hI : I ≠ 0) : ∃ a, I ⊔ span {a} = J. Apply it to I*J ≤ J (beware: here Ideal.mul_le_right : I * J ≤ J, mul_le_left : I * J ≤ I). Then (a) ≤ J gives (a) = J*K via Ideal.dvd_iff_le, so J*(I ⊔ K) = J*⊤ (Ideal.mul_sup, Ideal.mul_top), and mul_left_cancel₀ gives I ⊔ K = ⊤. Handle I = ⊤ separately, because then a may be 0. For coprime I, K an explicit iso I × K ≃ R × ↥(I*K) is (i,k) ↦ (i+k, i*y - x*k) where 1 = x + y. Prove map_add/smul with targeted simp only + ring, and left_inv/right_inv with show + linear_combination. Plain simp <;> ring on those subtype goals hit a whnf timeout.