-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
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)
have H : HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((Ideal.Quotient.mk (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) : (a : R) → R ⧸ I ^ n • ⊤) (f i) :
      R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) =
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (f i)
    (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
Tactic: simp only [algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, LinearMap.coe_comp,
    coe_lsum, LinearMap.coe_smul, LinearMap.id_coe, LinearEquiv.coe_coe, Function.comp_apply,
    finsuppLEquivDirectSum_symm_lof, Pi.smul_apply, id_eq, smul_zero, sum_single_index, smul_eval,
    mapQ_eq_factor, factor_eq_factor, of_apply, mkQ_apply, Ideal.Quotient.mk_eq_mk, mk_apply_coe,
    sumEquivOfFintype_apply, sum_lof, map_mk, AdicCauchySequence.map_apply_coe, map_smul]