-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : ι → R
H :
  ∀ (i : ι) (a : AdicCauchySequence I M) (n : ℕ),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      ((↑(((((lsum (AdicCompletion I R) :
                        (a : ι → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M) →
                          (ι →₀ AdicCompletion I M) →ₗ[AdicCompletion I R] AdicCompletion I M)
                      fun (i : ι) ↦
                      HSMul.hSMul (α := AdicCompletion I R) (β :=
                        LinearMap.{u_1, u_1, u_2, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
                          (AdicCompletion I M) (AdicCompletion I M))
                        ((algebraMap R (AdicCompletion I R) : (a : R) → AdicCompletion I R) (f i) : AdicCompletion I R)
                        LinearMap.id) ∘ₗ
                    (↑(LinearEquiv.symm (finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι)) :
                      (DirectSum ι fun (x : ι) ↦ AdicCompletion I M) →ₗ[AdicCompletion I R] ι →₀ AdicCompletion I M)) ∘ₗ
                  DirectSum.lof.{u_1, u_3, u_2} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I M) i :
                (a : AdicCompletion I M) → AdicCompletion I M)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → M ⧸ I ^ n • ⊤)
        n)
      ((↑(((((map I
                          ((lsum R : (a : ι → M →ₗ[R] M) → (ι →₀ M) →ₗ[R] M) fun (i : ι) ↦
                            HSMul.hSMul (β := M →ₗ[R] M) (f i) LinearMap.id) ∘ₗ
                        map I
                          (↑(LinearEquiv.symm (finsuppLEquivDirectSum R M ι)) :
                            (DirectSum ι fun (x : ι) ↦ M) →ₗ[R] ι →₀ M)) ∘ₗ
                      (↑(sumEquivOfFintype I fun (x : ι) ↦ M) :
                        (DirectSum ι fun (j : ι) ↦ AdicCompletion I M) →ₗ[AdicCompletion I R]
                          AdicCompletion I (DirectSum ι fun (j : ι) ↦ M))) ∘ₗ
                    DirectSum.lof.{u_1, u_3, u_2} (AdicCompletion I R) ι (fun (i : ι) ↦ AdicCompletion I M) i :
                  LinearMap.{u_1, u_1, u_2, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
                    (AdicCompletion I M) (AdicCompletion I M)) :
                (a : AdicCompletion I M) → AdicCompletion I M)
              ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a)) :
          (n : ℕ) → M ⧸ I ^ n • ⊤)
        n)
⊢ Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
      (DirectSum.{u_3, u_2} ι fun (x : ι) ↦ AdicCompletion I M) (AdicCompletion I M))
    (((lsum (AdicCompletion I R) :
          (a : ι → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M) →
            (ι →₀ AdicCompletion I M) →ₗ[AdicCompletion I R] AdicCompletion I M)
        fun (i : ι) ↦
        HSMul.hSMul (α := AdicCompletion I R) (β :=
          LinearMap.{u_1, u_1, u_2, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
            (AdicCompletion I M) (AdicCompletion I M))
          ((algebraMap R (AdicCompletion I R) : (a : R) → AdicCompletion I R) (f i) : AdicCompletion I R)
          LinearMap.id) ∘ₗ
      (↑(LinearEquiv.symm (finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι)) :
        (DirectSum ι fun (x : ι) ↦ AdicCompletion I M) →ₗ[AdicCompletion I R] ι →₀ AdicCompletion I M))
    ((map I
          ((lsum R : (a : ι → M →ₗ[R] M) → (ι →₀ M) →ₗ[R] M) fun (i : ι) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (f i) LinearMap.id) ∘ₗ
        map I (↑(LinearEquiv.symm (finsuppLEquivDirectSum R M ι)) : (DirectSum ι fun (x : ι) ↦ M) →ₗ[R] ι →₀ M)) ∘ₗ
      (↑(sumEquivOfFintype I fun (x : ι) ↦ M) :
        (DirectSum ι fun (j : ι) ↦ AdicCompletion I M) →ₗ[AdicCompletion I R]
          AdicCompletion I (DirectSum ι fun (j : ι) ↦ M)))

Tactic:
ext