-- 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
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ 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
have 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) ⊤)
Tactic: ext x