Exists adic Valued mul sub le

lemma exists_adicValued_mul_sub_le {a b : A} {γ : WithZero (Multiplicative ℤ)} (hγ : γ ≠ 0)    (hle : γ ≤ v.intValuation a)    (hle' : v.intValuation b ≤ v.intValuation a) :    ∃ y, v.intValuation (y * a - b) ≤ γ := by  -- Find `n` such that `γ = Multiplicative.ofAdd (-(n : ℤ))`  have hγ' : γ ≤ 1 := by    apply hle.trans    apply intValuation_le_one  obtain ⟨n, hn⟩ := exists_ofAdd_natCast_of_le_one hγ hγ'  rw [← hn, ← WithZero.exp] at hle ⊢  have hnz : a ≠ 0 := ne_zero_of_some_le_intValuation _ hle  have hnb : Ideal.span {a} ≠ ⊥ := by    rwa [ne_eq, Ideal.span_singleton_eq_bot]  -- Rewrite the statements to involve multiplicity rather than valuations  rw [intValuation_eq_coe_neg_multiplicity _ hnz, WithZero.exp_le_exp, neg_le_neg_iff,    Int.ofNat_le] at hle  have hm : emultiplicity v.asIdeal (Ideal.span {a}) ≤ n :=    le_of_eq_of_le      (emultiplicity_eq_of_valuation_eq_ofAdd v <| intValuation_eq_coe_neg_multiplicity v hnz)      (ENat.coe_le_coe.mpr hle)  have hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) := by    rwa [← intValuation_le_pow_iff_mem, ← intValuation_eq_coe_neg_multiplicity _ hnz]  -- Now make use of  -- `v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) = v.asIdeal ^ n ⊔ Ideal.span {a}`  -- (this is where we need `IsDedekindDomain A`)  rw [← Ideal.irreducible_pow_sup_of_ge hnb (irreducible v) n hm] at hb  -- Extract y by writing b as a general term of the sum of the two ideals.  obtain ⟨x, hx, z, hz, hxz⟩ := Submodule.mem_sup.mp hb  obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp hz  use y  -- And again prove the result about valuations by turning into one about ideals.  rwa [hy, ← hxz, sub_add_cancel_right, intValuation_le_pow_iff_mem, neg_mem_iff]