∀ {R : Type u_1} [inst : CommRing R] {A : outParam (Type u_2)} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {V : Type u_3} [inst_3 : AddCommMonoid V] [inst_4 : Module R V] [inst_5 : Module A V] [inst_6 : IsScalarTower R A V]
  [inst_7 : Algebra R A] [inst_8 : IsScalarTower R A V] {M : Submodule R V},
  M.FG → Submodule.span A ↑M = ⊤ → Submodule.IsLattice A M