∀ {R : Type u_2} [inst : CommRing R] (I : Ideal R) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x y : AdicCompletion I M) {m n : ℕ} (hmn : m ≤ n), (AdicCompletion.transitionMap I M hmn) ((↑x + ↑y) n) = (↑x + ↑y) m