∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsAdicComplete I M], AdicCompletion.ofLinearEquiv I M = LinearEquiv.ofBijective (AdicCompletion.of I M) ⋯