-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.NilpotentKer (goal)
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 • ⊤)
⊢ 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))
have 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₂)
            ψ)
          ⊤)
Tactic: convert! Module.Finite.fg_top.map (ψ.restrictScalars R) using 1