-- Module: Mathlib.RingTheory.AdicCompletion.Functoriality
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
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)
                  ⋯))
              (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)
                    ⋯))
                x)) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        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)
          ⋯))
      (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)

Tactic:
ext