-- 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
m n : ℕ
hmn : m ≤ n
rw :
  (transitionMap I N hmn ∘ₗ
        (↑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 =
    (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 :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M)
            (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)))
      m
rw₁ :
  Eq (α :=
    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M) (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_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 ^ m) f) ∘ₗ
        transitionMap I M hmn) ∘ₗ
      eval I M n)
    ((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 :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M)
            (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)))
      m)
rw₂ :
  Eq (α :=
    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M) (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_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 ^ m) f) ∘ₗ
      transitionMap I M hmn ∘ₗ eval I M n)
    ((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 :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M)
            (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)))
      m)
rw₃ rw₄ :
  Eq (α :=
    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M) (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_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 ^ m) f) ∘ₗ
      eval I M m)
    ((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 :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M)
            (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)))
      m)
⊢ Eq (α :=
    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M) (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤))
    (transitionMap I N hmn ∘ₗ
      (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 :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M)
              (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)))
        n)
    ((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 :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (AdicCompletion I M)
            (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)))
      m)

Tactic:
rw [← comp_assoc, AdicCompletion.transitionMap_comp_reduceModIdeal,
        comp_assoc, transitionMap_comp_eval]

Premises used: LinearMap.comp_assoc, AdicCompletion.transitionMap_comp_eval, AdicCompletion.transitionMap_comp_reduceModIdeal