-- 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
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
this :
  Function.Surjective (α := Finsupp.{u_1, u_2} (↥s) M) (β := ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    (⇑(LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
          ⋯) :
      (a : ↥s →₀ M) → ↥(I ^ n • ⊤))
x : AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M)
rw :
  Eq.{u_2 + 1} (α := AdicCompletion I M)
    ((map I
            ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
              HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((ofPowSMul I M n ∘ₗ
            map I
              (LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
                ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
                  HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
                ⋯) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
rw₁ :
  Eq.{u_2 + 1} (α := AdicCompletion I M)
    ((map I
            ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
              HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((map I
            ((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).subtype ∘ₗ
              LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
                ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
                  HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
                ⋯) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := AdicCompletion I M)
    ((map I
            ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
              HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((map I
            ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
              HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
⊢ Eq.{u_2 + 1} (α := AdicCompletion I M)
    ((map I
            ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
              HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M)
        ((map I
              (LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
                ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
                  HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
                ⋯) :
            (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I ↥(I ^ n • ⊤))
          x) :
      AdicCompletion I M)

Tactic:
rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]

Premises used: LinearMap.subtype_comp_codRestrict, AdicCompletion.map_comp, LinearMap.comp_apply