∀ {A : Type u_1} [inst : CommRing A] {g g_1 : PowerSeries A} (e_g : g = g_1) {I I_1 : Ideal A} (e_I : I = I_1)
  (H : g.IsWeierstrassDivisorAt I) (f f_1 : PowerSeries A),
  f = f_1 → ∀ [inst_1 : IsPrecomplete I A], H.mod f = ⋯.mod f_1