∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι]
  [inst_4 : Fintype ι],
  AdicCompletion.piEquivOfFintype I M =
    (AdicCompletion.congr I (DirectSum.linearEquivFunOnFintype R ι M)).symm.trans
      ((AdicCompletion.sumEquivOfFintype I M).symm.trans
        (DirectSum.linearEquivFunOnFintype (AdicCompletion I R) ι fun j => AdicCompletion I (M j)))