-- Module: Mathlib.RingTheory.Finiteness.NilpotentKer
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Module.Finite R T
f : S →ₐ[R] T
hf₁ : Function.Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := T) (⇑f : (a : S) → T)
I : Ideal S
hI : RingHom.ker f = I
hf₂ : I ≤ nilradical S
hf₃ : I.FG
this_1 : Module.Finite.{u_1, u_2} R (S ⧸ I)
n : ℕ
IH : Module.Finite.{u_1, u_2} R (S ⧸ I ^ n)
φ : S ⧸ I ^ (n + 1) →ₐ[S] S ⧸ I ^ n := Ideal.Quotient.factorₐ S ⋯
hφ : Function.Surjective (α := S ⧸ I ^ (n + 1)) (β := S ⧸ I ^ n) (⇑φ : (a : S ⧸ I ^ (n + 1)) → S ⧸ I ^ n)
hφ' : φ.toLinearMap ∘ₗ Submodule.mkQ (I ^ (n + 1)) = Submodule.mkQ (I ^ n)
this : Module.Finite.{u_1, u_2} R ((S ⧸ I) ⊗[S] ↥(I ^ n))
ψ : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] S ⧸ I ^ (n + 1) :=
  (HSMul.hSMul (β := Submodule S ↥(I ^ n)) I ⊤).liftQ (Submodule.mkQ (I ^ (n + 1)) ∘ₗ Submodule.subtype (I ^ n)) ⋯ ∘ₗ
    (↑(quotTensorEquivQuotSMul (↥(I ^ n)) I) : (S ⧸ I) ⊗[S] ↥(I ^ n) →ₗ[S] ↥(I ^ n) ⧸ I • ⊤)
h :
  Eq.{u_1 + 1} (α := Semiring R) Ring.toSemiring CommSemiring.toSemiring →
    Eq.{u_2 + 1} (α := AddCommMonoid (S ⧸ I ^ (n + 1))) AddCommGroup.toAddCommMonoid
        (Submodule.Quotient.addCommMonoid (I ^ (n + 1))) →
      HEq (α := Module.{u_1, u_2} R (S ⧸ I ^ (n + 1))) (Submodule.Quotient.module' (I ^ (n + 1))) (β :=
          Module.{u_1, u_2} R (S ⧸ I ^ (n + 1))) (Submodule.Quotient.module' (I ^ (n + 1))) →
        Eq (α := Submodule R (S ⧸ I ^ (n + 1)))
          (⊤ ⊓
            LinearMap.ker
              ((↑R :
                  {S M M₂ : Type u_2} →
                    [inst : Semiring R] →
                      [inst_6 : Semiring S] →
                        [inst_7 : AddCommMonoid M] →
                          [inst_8 : AddCommMonoid M₂] →
                            [inst_9 : Module R M] →
                              [inst_10 : Module R M₂] →
                                [inst_11 : Module S M] →
                                  [inst_12 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                φ.toLinearMap))
          (Submodule.map
            ((↑R :
                {S M M₂ : Type u_2} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              ψ)
            ⊤)
⊢ Submodule.FG
    (⊤ ⊓
      LinearMap.ker
        ((↑R :
            {S M M₂ : Type u_2} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          φ.toLinearMap))

Tactic:
convert! Module.Finite.fg_top.map (ψ.restrictScalars R) using 1

Premises used: Module.Finite.fg_top, LinearMap.restrictScalars, Submodule.FG.map