{A : Type u} →
  {inst : Ring A} →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        {inst_1 : AddCommGroup M₁} →
          {inst_2 : Module A M₁} →
            {inst_3 : AddCommGroup M₂} →
              {inst_4 : Module A M₂} →
                {pres₂ : Module.Presentation A M₂} →
                  {f : M₁ →ₗ[A] M₂} →
                    {ι : Type w₁} →
                      {g₁ : ι → M₁} → [SizeOf A] → [SizeOf M₁] → [SizeOf M₂] → [SizeOf ι] → pres₂.CokernelData f g₁ → ℕ