-- 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
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
      (((transitionMap I N hmn ∘ₗ
                (↑R :
                    {S : Type u_1} →
                      {M : Type u_2} →
                        {M₂ : Type u_3} →
                          [inst : Semiring R] →
                            [inst_5 : Semiring S] →
                              [inst_6 : AddCommMonoid M] →
                                [inst_7 : AddCommMonoid M₂] →
                                  [inst_8 : Module R M] →
                                    [inst_9 : Module R M₂] →
                                      [inst_10 : Module S M] →
                                        [inst_11 : Module S M₂] →
                                          [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (reduceModIdeal (I ^ n) f)) ∘ₗ
              (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ :
            (a : M) → N ⧸ I ^ m • ⊤)
          x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
      (((((↑R :
                      {S : Type u_1} →
                        {M : Type u_2} →
                          {M₂ : Type u_3} →
                            [inst : Semiring R] →
                              [inst_5 : Semiring S] →
                                [inst_6 : AddCommMonoid M] →
                                  [inst_7 : AddCommMonoid M₂] →
                                    [inst_8 : Module R M] →
                                      [inst_9 : Module R M₂] →
                                        [inst_10 : Module S M] →
                                          [inst_11 : Module S M₂] →
                                            [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (reduceModIdeal (I ^ m) f) ∘ₗ
                  transitionMap I M hmn) ∘ₗ
                (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).mkQ :
              LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)) :
            (a : M) → N ⧸ I ^ m • ⊤)
          x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤)
⊢ transitionMap I N hmn ∘ₗ
      (↑R :
          {S : Type u_1} →
            {M : Type u_2} →
              {M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (reduceModIdeal (I ^ n) f) =
    (↑R :
          {S : Type u_1} →
            {M : Type u_2} →
              {M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (reduceModIdeal (I ^ m) f) ∘ₗ
      transitionMap I M hmn

Tactic:
ext x