-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
r : AdicCompletion I R
x : AdicCompletion I M
⊢ AddHom.toFun
      (toAddHom
        (lift I
          (fun (n : ℕ) ↦
            (↑R :
                  {S : Type u_1} →
                    {M : Type u_2} →
                      {M₂ : Type u_3} →
                        [inst : Semiring R] →
                          [inst_9 : Semiring S] →
                            [inst_10 : AddCommMonoid M] →
                              [inst_11 : AddCommMonoid M₂] →
                                [inst_12 : Module R M] →
                                  [inst_13 : Module R M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (reduceModIdeal (I ^ n) f) ∘ₗ
              eval I M n)
          ⋯))
      (r • x) =
    HSMul.hSMul (α := AdicCompletion I R) (β := AdicCompletion I N)
      ((RingHom.id (AdicCompletion I R) : (a : AdicCompletion I R) → AdicCompletion I R) r : AdicCompletion I R)
      (AddHom.toFun
        (toAddHom
          (lift I
            (fun (n : ℕ) ↦
              (↑R :
                    {S : Type u_1} →
                      {M : Type u_2} →
                        {M₂ : Type u_3} →
                          [inst : Semiring R] →
                            [inst_9 : Semiring S] →
                              [inst_10 : AddCommMonoid M] →
                                [inst_11 : AddCommMonoid M₂] →
                                  [inst_12 : Module R M] →
                                    [inst_13 : Module R M₂] →
                                      [inst_14 : Module S M] →
                                        [inst_15 : Module S M₂] →
                                          [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (reduceModIdeal (I ^ n) f) ∘ₗ
                eval I M n)
            ⋯))
        x)
have h : ∀ (n : ℕ),
  (↑(AddHom.toFun
            (toAddHom
              (lift I
                (fun (n : ℕ) ↦
                  (↑R :
                        {S : Type u_1} →
                          {M : Type u_2} →
                            {M₂ : Type u_3} →
                              [inst : Semiring R] →
                                [inst_9 : Semiring S] →
                                  [inst_10 : AddCommMonoid M] →
                                    [inst_11 : AddCommMonoid M₂] →
                                      [inst_12 : Module R M] →
                                        [inst_13 : Module R M₂] →
                                          [inst_14 : Module S M] →
                                            [inst_15 : Module S M₂] →
                                              [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (reduceModIdeal (I ^ n) f) ∘ₗ
                    eval I M n)
                sorry))
            (r • x)) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n =
    (↑(HSMul.hSMul (α := AdicCompletion I R) (β := AdicCompletion I N)
            ((RingHom.id (AdicCompletion I R) : (a : AdicCompletion I R) → AdicCompletion I R) r : AdicCompletion I R)
            (AddHom.toFun
              (toAddHom
                (lift I
                  (fun (n : ℕ) ↦
                    (↑R :
                          {S : Type u_1} →
                            {M : Type u_2} →
                              {M₂ : Type u_3} →
                                [inst : Semiring R] →
                                  [inst_9 : Semiring S] →
                                    [inst_10 : AddCommMonoid M] →
                                      [inst_11 : AddCommMonoid M₂] →
                                        [inst_12 : Module R M] →
                                          [inst_13 : Module R M₂] →
                                            [inst_14 : Module S M] →
                                              [inst_15 : Module S M₂] →
                                                [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        (reduceModIdeal (I ^ n) f) ∘ₗ
                      eval I M n)
                  sorry))
              x)) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n
Tactic: ext